feat(*): misc simple lemmas (#2036)

* feat(*): misc simple lemmas

* +1 lemma

* Rename `inclusion_range` to `range_inclusion`

Co-Authored-By: Johan Commelin <johan@commelin.net>

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 3 people

src/analysis/normed_space/basic.lean

@@ -627,6 +627,10 @@ by simp only [dist_eq_norm, (norm_smul _ _).symm, smul_sub]
 lemma nnnorm_smul [normed_space α β] (s : α) (x : β) : nnnorm (s • x) = nnnorm s * nnnorm x :=
 nnreal.eq $ norm_smul s x
 
+lemma nndist_smul [normed_space α β] (s : α) (x y : β) :
+  nndist (s • x) (s • y) = nnnorm s * nndist x y :=
+nnreal.eq $ dist_smul s x y
+
 variables {E : Type*} {F : Type*}
 [normed_group E] [normed_space α E] [normed_group F] [normed_space α F]
 

src/data/set/basic.lean

@@ -1599,6 +1599,9 @@ lemma inclusion_injective {s t : set α} (h : s ⊆ t) :
   function.injective (inclusion h)
 | ⟨_, _⟩ ⟨_, _⟩ := subtype.ext.2 ∘ subtype.ext.1
 
+lemma range_inclusion {s t : set α} (h : s ⊆ t) : range (inclusion h) = {x : t | (x:α) ∈ s} :=
+ext $ λ ⟨x, hx⟩ , by simp [inclusion]
+
 end inclusion
 
 end set

src/order/filter/basic.lean

@@ -1066,6 +1066,10 @@ lemma comap_ne_bot_of_surj {f : filter β} {m : α → β}
   (hf : f ≠ ⊥) (hm : function.surjective m) : comap m f ≠ ⊥ :=
 comap_ne_bot_of_range_mem hf $ univ_mem_sets' hm
 
+lemma comap_ne_bot_of_image_mem {f : filter β} {m : α → β} (hf : f ≠ ⊥)
+  {s : set α} (hs : m '' s ∈ f) : comap m f ≠ ⊥ :=
+ne_bot_of_le_ne_bot (comap_inf_principal_ne_bot_of_image_mem hf hs) inf_le_left
+
 @[simp] lemma map_eq_bot_iff : map m f = ⊥ ↔ f = ⊥ :=
 ⟨by rw [←empty_in_sets_eq_bot, ←empty_in_sets_eq_bot]; exact id,
   assume h, by simp only [h, eq_self_iff_true, map_bot]⟩

src/topology/metric_space/emetric_space.lean

@@ -415,6 +415,10 @@ instance prod.emetric_space_max [emetric_space β] : emetric_space (α × β) :=
   end,
   to_uniform_space := prod.uniform_space }
 
+lemma prod.edist_eq [emetric_space β] (x y : α × β) :
+  edist x y = max (edist x.1 y.1) (edist x.2 y.2) :=
+rfl
+
 section pi
 open finset
 variables {π : β → Type*} [fintype β]
@@ -528,6 +532,10 @@ by simp [is_open_iff_nhds, mem_nhds_iff]
 theorem is_open_ball : is_open (ball x ε) :=
 is_open_iff.2 $ λ y, exists_ball_subset_ball
 
+theorem is_closed_ball_top : is_closed (ball x ⊤) :=
+is_open_iff.2 $ λ y hy, ⟨⊤, ennreal.coe_lt_top, subset_compl_iff_disjoint.2 $
+  ball_disjoint $ by { rw ennreal.top_add, exact le_of_not_lt hy }⟩
+
 theorem ball_mem_nhds (x : α) {ε : ennreal} (ε0 : 0 < ε) : ball x ε ∈ 𝓝 x :=
 mem_nhds_sets is_open_ball (mem_ball_self ε0)