feat(topology/separation): a cont. function with a cont. left inverse…

… is a closed embedding (#6329)

src/topology/continuous_on.lean

@@ -262,11 +262,16 @@ lemma eventually_nhds_with_of_forall {s : set α} {a : α} {p : α → Prop} (h
   ∀ᶠ x in 𝓝[s] a, p x :=
 mem_inf_sets_of_right h
 
-lemma tendsto_nhds_within_of_tendsto_nhds_of_eventually_within {β : Type*} {a : α} {l : filter β}
-  {s : set α} (f : β → α) (h1 : tendsto f l (nhds a)) (h2 : ∀ᶠ x in l, f x ∈ s) :
+lemma tendsto_nhds_within_of_tendsto_nhds_of_eventually_within {a : α} {l : filter β}
+  {s : set α} (f : β → α) (h1 : tendsto f l (𝓝 a)) (h2 : ∀ᶠ x in l, f x ∈ s) :
   tendsto f l (𝓝[s] a) :=
 tendsto_inf.2 ⟨h1, tendsto_principal.2 h2⟩
 
+@[simp] lemma tendsto_nhds_within_range {a : α} {l : filter β} {f : β → α} :
+  tendsto f l (𝓝[range f] a) ↔ tendsto f l (𝓝 a) :=
+⟨λ h, h.mono_right inf_le_left, λ h, tendsto_inf.2
+  ⟨h, tendsto_principal.2 $ eventually_of_forall mem_range_self⟩⟩
+
 lemma filter.eventually_eq.eq_of_nhds_within {s : set α} {f g : α → β} {a : α}
   (h : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : f a = g a :=
 h.self_of_nhds_within hmem

src/topology/local_homeomorph.lean

@@ -192,6 +192,10 @@ lemma map_nhds_eq (e : local_homeomorph α β) {x} (hx : x ∈ e.source) :
 le_antisymm (e.continuous_at hx) $
   le_map_of_right_inverse (e.eventually_right_inverse' hx) (e.tendsto_symm hx)
 
+lemma image_mem_nhds (e : local_homeomorph α β) {x} (hx : x ∈ e.source) {s : set α} (hs : s ∈ 𝓝 x) :
+  e '' s ∈ 𝓝 (e x) :=
+e.map_nhds_eq hx ▸ filter.image_mem_map hs
+
 /-- Preimage of interior or interior of preimage coincide for local homeomorphisms, when restricted
 to the source. -/
 lemma preimage_interior (s : set β) :

src/topology/maps.lean

@@ -126,6 +126,11 @@ lemma embedding_of_embedding_compose {f : α → β} {g : β → γ} (hf : conti
 { induced := (inducing_of_inducing_compose hf hg hgf.to_inducing).induced,
   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) :
+  embedding g :=
+embedding_of_embedding_compose hg hf $ h.comp_eq_id.symm ▸ embedding_id
+
 lemma embedding.map_nhds_eq {f : α → β} (hf : embedding f) (a : α) :
   (𝓝 a).map f = 𝓝[range f] (f a) :=
 hf.1.map_nhds_eq a
@@ -285,7 +290,7 @@ lemma of_inverse {f : α → β} {f' : β → α}
   is_closed_map f :=
 assume s hs,
 have f' ⁻¹' s = f '' s, by ext x; simp [mem_image_iff_of_inverse r_inv l_inv],
-this ▸ continuous_iff_is_closed.mp h s hs
+this ▸ hs.preimage h
 
 lemma of_nonempty {f : α → β} (h : ∀ s, is_closed s → s.nonempty → is_closed (f '' s)) :
   is_closed_map f :=

src/topology/separation.lean

@@ -477,6 +477,20 @@ lemma continuous.ext_on [t2_space α] {s : set β} (hs : dense s) {f g : β →
   f = g :=
 funext $ λ x, h.closure hf hg (hs x)
 
+lemma function.left_inverse.closed_range [t2_space α] {f : α → β} {g : β → α}
+  (h : function.left_inverse f g) (hf : continuous f) (hg : continuous g) :
+  is_closed (range g) :=
+have eq_on (g ∘ f) id (closure $ range g),
+  from h.right_inv_on_range.eq_on.closure (hg.comp hf) continuous_id,
+is_closed_of_closure_subset $ λ x hx,
+calc x = g (f x) : (this hx).symm
+   ... ∈ _ : mem_range_self _
+
+lemma function.left_inverse.closed_embedding [t2_space α] {f : α → β} {g : β → α}
+  (h : function.left_inverse f g) (hf : continuous f) (hg : continuous g) :
+  closed_embedding g :=
+⟨h.embedding hf hg, h.closed_range hf hg⟩
+
 lemma diagonal_eq_range_diagonal_map {α : Type*} : {p:α×α | p.1 = p.2} = range (λx, (x,x)) :=
 ext $ assume p, iff.intro
   (assume h, ⟨p.1, prod.ext_iff.2 ⟨rfl, h⟩⟩)
@@ -600,7 +614,7 @@ class regular_space (α : Type u) [topological_space α] extends t1_space α : P
 (regular : ∀{s:set α} {a}, is_closed s → a ∉ s → ∃t, is_open t ∧ s ⊆ t ∧ 𝓝[t] a = ⊥)
 
 lemma nhds_is_closed [regular_space α] {a : α} {s : set α} (h : s ∈ 𝓝 a) :
-  ∃t∈(𝓝 a), t ⊆ s ∧ is_closed t :=
+  ∃ t ∈ 𝓝 a, t ⊆ s ∧ is_closed t :=
 let ⟨s', h₁, h₂, h₃⟩ := mem_nhds_sets_iff.mp h in
 have ∃t, is_open t ∧ s'ᶜ ⊆ t ∧ 𝓝[t] a = ⊥,
   from regular_space.regular (is_closed_compl_iff.mpr h₂) (not_not_intro h₃),