feat(topology/maps): a few lemmas about is_open_map (#1855)

* feat(topology/maps): a few lemmas about `is_open_map`

Also fix arguments order in all `*.comp` in this file.

* Use restricted version of `continuous_of_left_inverse` to prove non-restricted

* Fix compile by reverting a name change

src/topology/constructions.lean

@@ -98,11 +98,11 @@ The 𝓝 filter and the subspace topology.
 
 theorem mem_nhds_subtype (s : set α) (a : {x // x ∈ s}) (t : set {x // x ∈ s}) :
   t ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 a.val, (@subtype.val α s) ⁻¹' u ⊆ t :=
-by rw mem_nhds_induced
+mem_nhds_induced subtype.val a t
 
 theorem nhds_subtype (s : set α) (a : {x // x ∈ s}) :
   𝓝 a = comap subtype.val (𝓝 a.val) :=
-by rw nhds_induced
+nhds_induced subtype.val a
 
 end topα
 
@@ -297,7 +297,7 @@ begin
   rw [is_open_map_iff_nhds_le],
   rintros ⟨a, b⟩,
   rw [nhds_prod_eq, nhds_prod_eq, ← filter.prod_map_map_eq],
-  exact filter.prod_mono ((is_open_map_iff_nhds_le f).1 hf a) ((is_open_map_iff_nhds_le g).1 hg b)
+  exact filter.prod_mono (is_open_map_iff_nhds_le.1 hf a) (is_open_map_iff_nhds_le.1 hg b)
 end
 
 protected lemma open_embedding.prod {f : α → β} {g : γ → δ}
@@ -370,13 +370,21 @@ lemma embedding_subtype_val : embedding (@subtype.val α p) :=
 lemma continuous_subtype_val : continuous (@subtype.val α p) :=
 continuous_induced_dom
 
-lemma subtype_val.open_embedding {s : set α} (hs : is_open s) :
-  open_embedding (subtype.val : {x // x ∈ s} → α) :=
+lemma is_open.open_embedding_subtype_val {s : set α} (hs : is_open s) :
+  open_embedding (subtype.val : s → α) :=
 { induced := rfl,
   inj := subtype.val_injective,
   open_range := (subtype.val_range : range subtype.val = s).symm ▸  hs }
 
-lemma subtype_val.closed_embedding {s : set α} (hs : is_closed s) :
+lemma is_open.is_open_map_subtype_val {s : set α} (hs : is_open s) :
+  is_open_map (subtype.val : s → α) :=
+hs.open_embedding_subtype_val.is_open_map
+
+lemma is_open_map.restrict {f : α → β} (hf : is_open_map f) {s : set α} (hs : is_open s) :
+  is_open_map (function.restrict f s) :=
+hf.comp hs.is_open_map_subtype_val
+
+lemma is_closed.closed_embedding_subtype_val {s : set α} (hs : is_closed s) :
   closed_embedding (subtype.val : {x // x ∈ s} → α) :=
 { induced := rfl,
   inj := subtype.val_injective,

src/topology/continuous_on.lean

@@ -337,6 +337,30 @@ begin
   exact (hf x hx).mem_closure_image hx
 end
 
+theorem is_open_map.continuous_on_image_of_left_inv_on {f : α → β} {s : set α}
+  (h : is_open_map (function.restrict f s)) {finv : β → α} (hleft : left_inv_on finv f s) :
+  continuous_on finv (f '' s) :=
+begin
+  rintros _ ⟨x, xs, rfl⟩ t ht,
+  rw [hleft x xs] at ht,
+  replace h := h.nhds_le ⟨x, xs⟩,
+  apply mem_nhds_within_of_mem_nhds,
+  apply h,
+  erw [map_compose.symm, function.comp, mem_map, ← nhds_within_eq_map_subtype_val],
+  apply mem_sets_of_superset (inter_mem_nhds_within _ ht),
+  assume y hy,
+  rw [mem_set_of_eq, mem_preimage, hleft _ hy.1],
+  exact hy.2
+end
+
+theorem is_open_map.continuous_on_range_of_left_inverse {f : α → β} (hf : is_open_map f)
+  {finv : β → α} (hleft : function.left_inverse finv f) :
+  continuous_on finv (range f) :=
+begin
+  rw [← image_univ],
+  exact (hf.restrict is_open_univ).continuous_on_image_of_left_inv_on (λ x _, hleft x)
+end
+
 lemma continuous_on.congr_mono {f g : α → β} {s s₁ : set α} (h : continuous_on f s)
   (h' : ∀x ∈ s₁, g x = f x) (h₁ : s₁ ⊆ s) : continuous_on g s₁ :=
 begin

src/topology/maps.lean

@@ -55,7 +55,7 @@ variables [topological_space α] [topological_space β] [topological_space γ] [
 lemma inducing_id : inducing (@id α) :=
 ⟨induced_id.symm⟩
 
-lemma inducing.comp {f : α → β} {g : β → γ} (hg : inducing g) (hf : inducing f) :
+protected lemma inducing.comp {g : β → γ} {f : α → β} (hg : inducing g) (hf : inducing f) :
   inducing (g ∘ f) :=
 ⟨by rw [hf.induced, hg.induced, induced_compose]⟩
 
@@ -114,7 +114,7 @@ lemma embedding.mk' (f : α → β) (inj : function.injective f)
 lemma embedding_id : embedding (@id α) :=
 ⟨inducing_id, assume a₁ a₂ h, h⟩
 
-lemma embedding.comp {f : α → β} {g : β → γ} (hg : embedding g) (hf : embedding f) :
+lemma embedding.comp {g : β → γ} {f : α → β} (hg : embedding g) (hf : embedding f) :
   embedding (g ∘ f) :=
 { inj:= assume a₁ a₂ h, hf.inj $ hg.inj h,
   ..hg.to_inducing.comp hf.to_inducing }
@@ -157,7 +157,8 @@ end embedding
 
 /-- A function between topological spaces is a quotient map if it is surjective,
   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 :=
+def quotient_map {α : Type*} {β : Type*} [tα : topological_space α] [tβ : topological_space β]
+  (f : α → β) : Prop :=
 function.surjective f ∧ tβ = tα.coinduced f
 
 namespace quotient_map
@@ -166,7 +167,7 @@ variables [topological_space α] [topological_space β] [topological_space γ] [
 protected lemma id : quotient_map (@id α) :=
 ⟨assume a, ⟨a, rfl⟩, coinduced_id.symm⟩
 
-protected lemma comp {f : α → β} {g : β → γ} (hf : quotient_map f) (hg : quotient_map g) :
+protected lemma comp {g : β → γ} {f : α → β} (hg : quotient_map g) (hf : quotient_map f) :
   quotient_map (g ∘ f) :=
 ⟨function.surjective_comp hg.left hf.left, by rw [hg.right, hf.right, coinduced_compose]⟩
 
@@ -191,9 +192,13 @@ end quotient_map
 section is_open_map
 variables [topological_space α] [topological_space β]
 
+/-- A map `f : α → β` is said to be an *open map*, if the image of any open `U : set α`
+is open in `β`. -/
 def is_open_map (f : α → β) := ∀ U : set α, is_open U → is_open (f '' U)
 
-lemma is_open_map_iff_nhds_le (f : α → β) : is_open_map f ↔ ∀(a:α), 𝓝 (f a) ≤ (𝓝 a).map f :=
+variable {f : α → β}
+
+lemma is_open_map_iff_nhds_le : is_open_map f ↔ ∀(a:α), 𝓝 (f a) ≤ (𝓝 a).map f :=
 begin
   split,
   { assume h a s hs,
@@ -215,9 +220,15 @@ open function
 protected lemma id : is_open_map (@id α) := assume s hs, by rwa [image_id]
 
 protected lemma comp
-  {f : α → β} {g : β → γ} (hf : is_open_map f) (hg : is_open_map g) : is_open_map (g ∘ f) :=
+  {g : β → γ} {f : α → β} (hg : is_open_map g) (hf : is_open_map f) : is_open_map (g ∘ f) :=
 by intros s hs; rw [image_comp]; exact hg _ (hf _ hs)
 
+lemma is_open_range {f : α → β} (hf : is_open_map f) : is_open (range f) :=
+by { rw ← image_univ, exact hf _ is_open_univ }
+
+lemma nhds_le {f : α → β} (hf : is_open_map f) (a : α) : 𝓝 (f a) ≤ (𝓝 a).map f :=
+is_open_map_iff_nhds_le.1 hf a
+
 lemma of_inverse {f : α → β} {f' : β → α}
   (h : continuous f') (l_inv : left_inverse f f') (r_inv : right_inverse f f') :
   is_open_map f :=
@@ -255,7 +266,7 @@ open function
 
 protected lemma id : is_closed_map (@id α) := assume s hs, by rwa image_id
 
-protected lemma comp {f : α → β} {g : β → γ} (hf : is_closed_map f) (hg : is_closed_map g) :
+protected lemma comp {g : β → γ} {f : α → β} (hg : is_closed_map g) (hf : is_closed_map f) :
   is_closed_map (g ∘ f) :=
 by { intros s hs, rw image_comp, exact hg _ (hf _ hs) }
 
@@ -315,7 +326,7 @@ end
 lemma open_embedding_id : open_embedding (@id α) :=
 ⟨embedding_id, by convert is_open_univ; apply range_id⟩
 
-lemma open_embedding.comp {f : α → β} {g : β → γ}
+lemma open_embedding.comp {g : β → γ} {f : α → β}
   (hg : open_embedding g) (hf : open_embedding f) : open_embedding (g ∘ f) :=
 ⟨hg.1.comp hf.1, show is_open (range (g ∘ f)),
  by rw [range_comp, ←hg.open_iff_image_open]; exact hf.2⟩
@@ -373,7 +384,7 @@ end
 lemma closed_embedding_id : closed_embedding (@id α) :=
 ⟨embedding_id, by convert is_closed_univ; apply range_id⟩
 
-lemma closed_embedding.comp {f : α → β} {g : β → γ}
+lemma closed_embedding.comp {g : β → γ} {f : α → β}
   (hg : closed_embedding g) (hf : closed_embedding f) : closed_embedding (g ∘ f) :=
 ⟨hg.to_embedding.comp hf.to_embedding, show is_closed (range (g ∘ f)),
  by rw [range_comp, ←hg.closed_iff_image_closed]; exact hf.closed_range⟩