feat(topology/maps): add 2 lemmas, open function (#15612)

* Add `is_open_map.of_inverse` and `is_open_map.range_mem_nhds`.
* Open namespace `function`, add `_root_` before `embedding` here and there.

One lemma comes from a recent presentation at Brown University, another one comes from the sphere eversion project.

src/topology/maps.lean

@@ -41,7 +41,7 @@ open map, closed map, embedding, quotient map, identification map
 
 -/
 
-open set filter
+open set filter function
 open_locale topological_space filter
 
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
@@ -145,17 +145,17 @@ section embedding
   and for all `s : set α`, `s` is open iff it is the preimage of an open set. -/
 @[mk_iff] structure embedding [tα : topological_space α] [tβ : topological_space β] (f : α → β)
   extends inducing f : Prop :=
-(inj : function.injective f)
+(inj : injective f)
 
 lemma function.injective.embedding_induced [t : topological_space β]
-  {f : α → β} (hf : function.injective f) :
-  @embedding α β (t.induced f) t f :=
+  {f : α → β} (hf : injective f) :
+  @_root_.embedding α β (t.induced f) t f :=
 { induced := rfl,
   inj := hf }
 
 variables [topological_space α] [topological_space β] [topological_space γ]
 
-lemma embedding.mk' (f : α → β) (inj : function.injective f)
+lemma embedding.mk' (f : α → β) (inj : injective f)
   (induced : ∀ a, comap f (𝓝 (f a)) = 𝓝 a) : embedding f :=
 ⟨inducing_iff_nhds.2 (λ a, (induced a).symm), inj⟩
 
@@ -173,7 +173,7 @@ lemma embedding_of_embedding_compose {f : α → β} {g : β → γ} (hf : conti
   inj := assume a₁ a₂ h, hgf.inj $ by simp [h, (∘)] }
 
 protected lemma function.left_inverse.embedding {f : α → β} {g : β → α}
-  (h : function.left_inverse f g) (hf : continuous f) (hg : continuous g) :
+  (h : left_inverse f g) (hf : continuous f) (hg : continuous g) :
   embedding g :=
 embedding_of_embedding_compose hg hf $ h.comp_eq_id.symm ▸ embedding_id
 
@@ -207,10 +207,10 @@ end embedding
   and for all `s : set β`, `s` is open iff its preimage is an open set. -/
 def quotient_map {α : Type*} {β : Type*} [tα : topological_space α] [tβ : topological_space β]
   (f : α → β) : Prop :=
-function.surjective f ∧ tβ = tα.coinduced f
+surjective f ∧ tβ = tα.coinduced f
 
 lemma quotient_map_iff {α β : Type*} [topological_space α] [topological_space β] {f : α → β} :
-  quotient_map f ↔ function.surjective f ∧ ∀ s : set β, is_open s ↔ is_open (f ⁻¹' s) :=
+  quotient_map f ↔ surjective f ∧ ∀ s : set β, is_open s ↔ is_open (f ⁻¹' s) :=
 and_congr iff.rfl topological_space_eq_iff
 
 namespace quotient_map
@@ -232,14 +232,18 @@ protected lemma of_quotient_map_compose (hf : continuous f) (hg : continuous g)
     (by { rw [hgf.right, ← continuous_iff_coinduced_le], apply continuous_coinduced_rng.comp hf })
     (by rwa ← continuous_iff_coinduced_le)⟩
 
+lemma of_inverse {g : β → α} (hf : continuous f) (hg : continuous g) (h : left_inverse g f) :
+  quotient_map g :=
+quotient_map.of_quotient_map_compose hf hg $ h.comp_eq_id.symm ▸ quotient_map.id
+
 protected lemma continuous_iff (hf : quotient_map f) :
   continuous g ↔ continuous (g ∘ f) :=
 by rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.right, coinduced_compose]
 
 protected lemma continuous (hf : quotient_map f) : continuous f :=
 hf.continuous_iff.mp continuous_id
 
-protected lemma surjective (hf : quotient_map f) : function.surjective f := hf.1
+protected lemma surjective (hf : quotient_map f) : surjective f := hf.1
 
 protected lemma is_open_preimage (hf : quotient_map f) {s : set β} :
   is_open (f ⁻¹' s) ↔ is_open s :=
@@ -258,7 +262,6 @@ def is_open_map [topological_space α] [topological_space β] (f : α → β) :=
 
 namespace is_open_map
 variables [topological_space α] [topological_space β] [topological_space γ] {f : α → β}
-open function
 
 protected lemma id : is_open_map (@id α) := assume s hs, by rwa [image_id]
 
@@ -274,6 +277,9 @@ lemma image_mem_nhds (hf : is_open_map f) {x : α} {s : set α} (hx : s ∈ 𝓝
 let ⟨t, hts, ht, hxt⟩ := mem_nhds_iff.1 hx in
 mem_of_superset (is_open.mem_nhds (hf t ht) (mem_image_of_mem _ hxt)) (image_subset _ hts)
 
+lemma range_mem_nhds (hf : is_open_map f) (x : α) : range f ∈ 𝓝 (f x) :=
+hf.is_open_range.mem_nhds $ mem_range_self _
+
 lemma maps_to_interior (hf : is_open_map f) {s : set α} {t : set β} (h : maps_to f s t) :
   maps_to f (interior s) (interior t) :=
 maps_to'.2 $ interior_maximal (h.mono interior_subset subset.rfl).image_subset
@@ -423,7 +429,7 @@ section open_embedding
 variables [topological_space α] [topological_space β] [topological_space γ]
 
 /-- An open embedding is an embedding with open image. -/
-structure open_embedding (f : α → β) extends embedding f : Prop :=
+structure open_embedding (f : α → β) extends _root_.embedding f : Prop :=
 (open_range : is_open $ range f)
 
 lemma open_embedding.is_open_map {f : α → β} (hf : open_embedding f) : is_open_map f :=
@@ -465,15 +471,15 @@ lemma open_embedding_iff_embedding_open {f : α → β} :
 ⟨λ h, ⟨h.1, h.is_open_map⟩, λ h, open_embedding_of_embedding_open h.1 h.2⟩
 
 lemma open_embedding_of_continuous_injective_open {f : α → β} (h₁ : continuous f)
-  (h₂ : function.injective f) (h₃ : is_open_map f) : open_embedding f :=
+  (h₂ : injective f) (h₃ : is_open_map f) : open_embedding f :=
 begin
   simp only [open_embedding_iff_embedding_open, embedding_iff, inducing_iff_nhds, *, and_true],
   exact λ a, le_antisymm (h₁.tendsto _).le_comap
     (@comap_map _ _ (𝓝 a) _ h₂ ▸ comap_mono (h₃.nhds_le _))
 end
 
 lemma open_embedding_iff_continuous_injective_open {f : α → β} :
-  open_embedding f ↔ continuous f ∧ function.injective f ∧ is_open_map f :=
+  open_embedding f ↔ continuous f ∧ injective f ∧ is_open_map f :=
 ⟨λ h, ⟨h.continuous, h.inj, h.is_open_map⟩,
   λ h, open_embedding_of_continuous_injective_open h.1 h.2.1 h.2.2⟩
 
@@ -504,7 +510,7 @@ section closed_embedding
 variables [topological_space α] [topological_space β] [topological_space γ]
 
 /-- A closed embedding is an embedding with closed image. -/
-structure closed_embedding (f : α → β) extends embedding f : Prop :=
+structure closed_embedding (f : α → β) extends _root_.embedding f : Prop :=
 (closed_range : is_closed $ range f)
 
 variables {f : α → β}
@@ -540,7 +546,7 @@ lemma closed_embedding_of_embedding_closed (h₁ : embedding f)
 ⟨h₁, by convert h₂ univ is_closed_univ; simp⟩
 
 lemma closed_embedding_of_continuous_injective_closed (h₁ : continuous f)
-  (h₂ : function.injective f) (h₃ : is_closed_map f) : closed_embedding f :=
+  (h₂ : injective f) (h₃ : is_closed_map f) : closed_embedding f :=
 begin
   refine closed_embedding_of_embedding_closed ⟨⟨_⟩, h₂⟩ h₃,
   apply le_antisymm (continuous_iff_le_induced.mp h₁) _,