feat(topology): some improvements (#11424)

* Prove a better version of `continuous_on.comp_fract`. Rename `continuous_on.comp_fract` -> `continuous_on.comp_fract''`.
* Rename `finset.closure_Union` -> `finset.closure_bUnion`
* Add `continuous.congr` and `continuous.subtype_coe`

src/topology/algebra/floor_ring.lean

@@ -26,7 +26,7 @@ This file proves statements about limits and continuity of functions involving `
 open filter function int set
 open_locale topological_space
 
-variables {α : Type*} [linear_ordered_ring α] [floor_ring α]
+variables {α β γ : Type*} [linear_ordered_ring α] [floor_ring α]
 
 lemma tendsto_floor_at_top : tendsto (floor : α → ℤ) at_top at_top :=
 floor_mono.tendsto_at_top_at_top $ λ b, ⟨(b + 1 : ℤ), by { rw floor_coe, exact (lt_add_one _).le }⟩
@@ -154,8 +154,10 @@ tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _
 
 local notation `I` := (Icc 0 1 : set α)
 
-lemma continuous_on.comp_fract' {β γ : Type*} [order_topology α]
-  [topological_add_group α] [topological_space β] [topological_space γ] {f : β → α → γ}
+variables [order_topology α] [topological_add_group α] [topological_space β] [topological_space γ]
+
+/-- Do not use this, use `continuous_on.comp_fract` instead. -/
+lemma continuous_on.comp_fract' {f : β → α → γ}
   (h : continuous_on (uncurry f) $ (univ : set β) ×ˢ I) (hf : ∀ s, f s 0 = f s 1) :
   continuous (λ st : β × α, f st.1 $ fract st.2) :=
 begin
@@ -198,23 +200,17 @@ begin
               (eventually_of_forall (λ x, ⟨fract_nonneg _, (fract_lt_one _).le⟩)) ) }
 end
 
-lemma continuous_on.comp_fract {β : Type*} [order_topology α]
-  [topological_add_group α] [topological_space β] {f : α → β}
-  (h : continuous_on f I) (hf : f 0 = f 1) : continuous (f ∘ fract) :=
-begin
-  let f' : unit → α → β := λ x y, f y,
-  have : continuous_on (uncurry f') ((univ : set unit) ×ˢ I),
-  { rintros ⟨s, t⟩ ⟨-, ht : t ∈ I⟩,
-    simp only [continuous_within_at, uncurry, nhds_within_prod_eq, nhds_within_univ, f'],
-    rw tendsto_prod_iff,
-    intros W hW,
-    specialize h t ht hW,
-    rw mem_map_iff_exists_image at h,
-    rcases h with ⟨V, hV, hVW⟩,
-    rw image_subset_iff at hVW,
-    use [univ, univ_mem, V, hV],
-    intros x y hx hy,
-    exact hVW hy },
-  have key : continuous (λ s, ⟨unit.star, s⟩ : α → unit × α) := by continuity,
-  exact (this.comp_fract' (λ s, hf)).comp key
-end
+lemma continuous_on.comp_fract
+  {s : β → α}
+  {f : β → α → γ}
+  (h : continuous_on (uncurry f) $ (univ : set β) ×ˢ (Icc 0 1 : set α))
+  (hs : continuous s)
+  (hf : ∀ s, f s 0 = f s 1) :
+  continuous (λ x : β, f x $ int.fract (s x)) :=
+(h.comp_fract' hf).comp (continuous_id.prod_mk hs)
+
+/-- A special case of `continuous_on.comp_fract`. -/
+lemma continuous_on.comp_fract'' {f : α → β} (h : continuous_on f I) (hf : f 0 = f 1) :
+  continuous (f ∘ fract) :=
+continuous_on.comp_fract (h.comp continuous_on_snd $ λ x hx, (mem_prod.mp hx).2)
+  continuous_id (λ _, hf)

src/topology/basic.lean

@@ -398,7 +398,7 @@ subset.antisymm
     is_closed.union is_closed_closure is_closed_closure)
   ((monotone_closure α).le_map_sup s t)
 
-@[simp] lemma finset.closure_Union {ι : Type*} (s : finset ι) (f : ι → set α) :
+@[simp] lemma finset.closure_bUnion {ι : Type*} (s : finset ι) (f : ι → set α) :
   closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i) :=
 begin
   classical,
@@ -409,7 +409,7 @@ end
 
 @[simp] lemma closure_Union_of_fintype {ι : Type*} [fintype ι] (f : ι → set α) :
   closure (⋃ i, f i) = ⋃ i, closure (f i) :=
-by { convert finset.univ.closure_Union f; simp, }
+by { convert finset.univ.closure_bUnion f; simp, }
 
 lemma interior_subset_closure {s : set α} : interior s ⊆ closure s :=
 subset.trans interior_subset subset_closure
@@ -1222,6 +1222,9 @@ lemma is_open.preimage {f : α → β} (hf : continuous f) {s : set β} (h : is_
   is_open (f ⁻¹' s) :=
 hf.is_open_preimage s h
 
+lemma continuous.congr {f g : α → β} (h : continuous f) (h' : ∀ x, f x = g x) : continuous g :=
+by { convert h, ext, rw h' }
+
 /-- A function between topological spaces is continuous at a point `x₀`
 if `f x` tends to `f x₀` when `x` tends to `x₀`. -/
 def continuous_at (f : α → β) (x : α) := tendsto f (𝓝 x) (𝓝 (f x))

src/topology/constructions.lean

@@ -641,6 +641,10 @@ continuous_induced_dom
 lemma continuous_subtype_coe : continuous (coe : subtype p → α) :=
 continuous_subtype_val
 
+lemma continuous.subtype_coe {f : β → subtype p} (hf : continuous f) :
+  continuous (λ x, (f x : α)) :=
+continuous_subtype_coe.comp hf
+
 lemma is_open.open_embedding_subtype_coe {s : set α} (hs : is_open s) :
   open_embedding (coe : s → α) :=
 { induced := rfl,