chore(topology/maps): golf, use section vars (#10747)

Also add `quotient_map.is_closed_preimage`

src/topology/maps.lean

@@ -98,7 +98,7 @@ lemma inducing.continuous_at_iff' {f : α → β} {g : β → γ} (hf : inducing
   (h : range f ∈ 𝓝 (f x)) : continuous_at (g ∘ f) x ↔ continuous_at g (f x) :=
 by { simp_rw [continuous_at, filter.tendsto, ← hf.map_nhds_of_mem _ h, filter.map_map] }
 
-lemma inducing.continuous {f : α → β} (hf : inducing f) : continuous f :=
+protected lemma inducing.continuous {f : α → β} (hf : inducing f) : continuous f :=
 hf.continuous_iff.mp continuous_id
 
 lemma inducing.closure_eq_preimage_closure_image {f : α → β} (hf : inducing f) (s : set α) :
@@ -184,37 +184,41 @@ lemma quotient_map_iff {α β : Type*} [topological_space α] [topological_space
 and_congr iff.rfl topological_space_eq_iff
 
 namespace quotient_map
+
 variables [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]
+  {g : β → γ} {f : α → β}
 
 protected lemma id : quotient_map (@id α) :=
 ⟨assume a, ⟨a, rfl⟩, coinduced_id.symm⟩
 
-protected lemma comp {g : β → γ} {f : α → β} (hg : quotient_map g) (hf : quotient_map f) :
+protected lemma comp (hg : quotient_map g) (hf : quotient_map f) :
   quotient_map (g ∘ f) :=
 ⟨hg.left.comp hf.left, by rw [hg.right, hf.right, coinduced_compose]⟩
 
-protected lemma of_quotient_map_compose {f : α → β} {g : β → γ}
-  (hf : continuous f) (hg : continuous g)
+protected lemma of_quotient_map_compose (hf : continuous f) (hg : continuous g)
   (hgf : quotient_map (g ∘ f)) : quotient_map g :=
-⟨assume b, let ⟨a, h⟩ := hgf.left b in ⟨f a, h⟩,
+⟨hgf.1.of_comp,
   le_antisymm
-    (by rw [hgf.right, ← continuous_iff_coinduced_le];
-        apply continuous_coinduced_rng.comp hf)
+    (by { rw [hgf.right, ← continuous_iff_coinduced_le], apply continuous_coinduced_rng.comp hf })
     (by rwa ← continuous_iff_coinduced_le)⟩
 
-protected lemma continuous_iff {f : α → β} {g : β → γ} (hf : quotient_map f) :
+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 {f : α → β} (hf : quotient_map f) : continuous f :=
+protected lemma continuous (hf : quotient_map f) : continuous f :=
 hf.continuous_iff.mp continuous_id
 
-protected lemma surjective {f : α → β} (hf : quotient_map f) : function.surjective f := hf.1
+protected lemma surjective (hf : quotient_map f) : function.surjective f := hf.1
 
-protected lemma is_open_preimage {f : α → β} (hf : quotient_map f) {s : set β} :
+protected lemma is_open_preimage (hf : quotient_map f) {s : set β} :
   is_open (f ⁻¹' s) ↔ is_open s :=
 ((quotient_map_iff.1 hf).2 s).symm
 
+protected lemma is_closed_preimage (hf : quotient_map f) {s : set β} :
+  is_closed (f ⁻¹' s) ↔ is_closed s :=
+by simp only [← is_open_compl_iff, ← preimage_compl, hf.is_open_preimage]
+
 end quotient_map
 
 /-- A map `f : α → β` is said to be an *open map*, if the image of any open `U : set α`
@@ -260,19 +264,11 @@ begin
   exact hs.preimage h
 end
 
+/-- A continuous surjective open map is a quotient map. -/
 lemma to_quotient_map {f : α → β}
-  (open_map : is_open_map f) (cont : continuous f) (surj : function.surjective f) :
+  (open_map : is_open_map f) (cont : continuous f) (surj : surjective f) :
   quotient_map f :=
-⟨ surj,
-  begin
-    ext s,
-    show is_open s ↔ is_open (f ⁻¹' s),
-    split,
-    { exact continuous_def.1 cont s },
-    { assume h,
-      rw ← surj.image_preimage s,
-      exact open_map _ h }
-  end⟩
+quotient_map_iff.2 ⟨surj, λ s, ⟨λ h, h.preimage cont, λ h, surj.image_preimage s ▸ open_map _ h⟩⟩
 
 lemma interior_preimage_subset_preimage_interior {s : set β} (hf : is_open_map f) :
   interior (f⁻¹' s) ⊆ f⁻¹' (interior s) :=
@@ -302,7 +298,8 @@ lemma is_open_map_iff_interior [topological_space α] [topological_space β] {f
   calc f '' u = f '' (interior u) : by rw hu.interior_eq
           ... ⊆ interior (f '' u) : hs u⟩
 
-lemma inducing.is_open_map [topological_space α] [topological_space β] {f : α → β}
+/-- An inducing map with an open range is an open map. -/
+protected lemma inducing.is_open_map [topological_space α] [topological_space β] {f : α → β}
   (hi : inducing f) (ho : is_open (range f)) :
   is_open_map f :=
 is_open_map.of_nhds_le $ λ x, (hi.map_nhds_of_mem _ $ is_open.mem_nhds ho $ mem_range_self _).ge
@@ -357,7 +354,7 @@ begin
   intros s hs,
   rcases hf.is_closed_iff.1 hs with ⟨t, ht, rfl⟩,
   rw image_preimage_eq_inter_range,
-  exact is_closed.inter ht h
+  exact ht.inter h
 end
 
 lemma is_closed_map_iff_closure_image [topological_space α] [topological_space β] {f : α → β} :
@@ -420,12 +417,11 @@ begin
 end
 
 lemma open_embedding_id : open_embedding (@id α) :=
-⟨embedding_id, by convert is_open_univ; apply range_id⟩
+⟨embedding_id, is_open_map.id.is_open_range⟩
 
 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⟩
+⟨hg.1.comp hf.1, (hg.is_open_map.comp hf.is_open_map).is_open_range⟩
 
 end open_embedding