feat(topology): various additions (#4264)

Some if it is used for Fubini, but some of the results were rabbit holes I went into, which I never ended up using, but that still seem useful.

src/order/liminf_limsup.lean

@@ -37,7 +37,7 @@ In complete lattices, however, it coincides with the `Inf Sup` definition.
 open filter set
 open_locale filter
 
-variables {α : Type*} {β : Type*}
+variables {α β ι : Type*}
 namespace filter
 
 section relation
@@ -317,36 +317,48 @@ le_antisymm
   (le_Inf $ assume a ha, let ⟨i, hi, ha⟩ := h.eventually_iff.1 ha in
     infi_le_of_le _ $ infi_le_of_le hi $ Sup_le ha)
 
+theorem has_basis.Liminf_eq_supr_Inf {p : ι → Prop} {s : ι → set α} {f : filter α}
+  (h : f.has_basis p s) : f.Liminf = ⨆ i (hi : p i), Inf (s i) :=
+@has_basis.Limsup_eq_infi_Sup (order_dual α) _ _ _ _ _ h
+
 theorem Limsup_eq_infi_Sup {f : filter α} : f.Limsup = ⨅ s ∈ f, Sup s :=
 f.basis_sets.Limsup_eq_infi_Sup
 
+theorem Liminf_eq_supr_Inf {f : filter α} : f.Liminf = ⨆ s ∈ f, Inf s :=
+@Limsup_eq_infi_Sup (order_dual α) _ _
+
 /-- In a complete lattice, the limsup of a function is the infimum over sets `s` in the filter
 of the supremum of the function over `s` -/
 theorem limsup_eq_infi_supr {f : filter β} {u : β → α} : f.limsup u = ⨅ s ∈ f, ⨆ a ∈ s, u a :=
 (f.basis_sets.map u).Limsup_eq_infi_Sup.trans $
   by simp only [Sup_image, id]
 
-lemma limsup_eq_infi_supr_of_nat {u : ℕ → α} : limsup at_top u = ⨅n:ℕ, ⨆i≥n, u i :=
+lemma limsup_eq_infi_supr_of_nat {u : ℕ → α} : limsup at_top u = ⨅ n : ℕ, ⨆ i ≥ n, u i :=
 (at_top_basis.map u).Limsup_eq_infi_Sup.trans $
   by simp only [Sup_image, infi_const]; refl
 
-lemma limsup_eq_infi_supr_of_nat' {u : ℕ → α} : limsup at_top u = ⨅n:ℕ, ⨆i, u (i + n) :=
+lemma limsup_eq_infi_supr_of_nat' {u : ℕ → α} : limsup at_top u = ⨅ n : ℕ, ⨆ i : ℕ, u (i + n) :=
 by simp only [limsup_eq_infi_supr_of_nat, supr_ge_eq_supr_nat_add]
 
-theorem Liminf_eq_supr_Inf {f : filter α} : f.Liminf = ⨆ s ∈ f, Inf s :=
-@Limsup_eq_infi_Sup (order_dual α) _ _
+theorem has_basis.limsup_eq_infi_supr {p : ι → Prop} {s : ι → set β} {f : filter β} {u : β → α}
+  (h : f.has_basis p s) : f.limsup u = ⨅ i (hi : p i), ⨆ a ∈ s i, u a :=
+(h.map u).Limsup_eq_infi_Sup.trans $ by simp only [Sup_image, id]
 
 /-- In a complete lattice, the liminf of a function is the infimum over sets `s` in the filter
 of the supremum of the function over `s` -/
 theorem liminf_eq_supr_infi {f : filter β} {u : β → α} : f.liminf u = ⨆ s ∈ f, ⨅ a ∈ s, u a :=
 @limsup_eq_infi_supr (order_dual α) β _ _ _
 
-lemma liminf_eq_supr_infi_of_nat {u : ℕ → α} : liminf at_top u = ⨆n:ℕ, ⨅i≥n, u i :=
+lemma liminf_eq_supr_infi_of_nat {u : ℕ → α} : liminf at_top u = ⨆ n : ℕ, ⨅ i ≥ n, u i :=
 @limsup_eq_infi_supr_of_nat (order_dual α) _ u
 
-lemma liminf_eq_supr_infi_of_nat' {u : ℕ → α} : liminf at_top u = ⨆n:ℕ, ⨅i, u (i + n) :=
+lemma liminf_eq_supr_infi_of_nat' {u : ℕ → α} : liminf at_top u = ⨆ n : ℕ, ⨅ i : ℕ, u (i + n) :=
 @limsup_eq_infi_supr_of_nat' (order_dual α) _ _
 
+theorem has_basis.liminf_eq_supr_infi {p : ι → Prop} {s : ι → set β} {f : filter β} {u : β → α}
+  (h : f.has_basis p s) : f.liminf u = ⨆ i (hi : p i), ⨅ a ∈ s i, u a :=
+@has_basis.limsup_eq_infi_supr (order_dual α) _ _ _ _ _ _ _ h
+
 end complete_lattice
 
 section conditionally_complete_linear_order

src/topology/algebra/infinite_sum.lean

@@ -436,6 +436,22 @@ end encodable
 
 end tsum
 
+section pi
+variables {ι : Type*} {π : α → Type*} [∀ x, add_comm_monoid (π x)] [∀ x, topological_space (π x)]
+
+lemma pi.has_sum {f : ι → ∀ x, π x} {g : ∀ x, π x} :
+  has_sum f g ↔ ∀ x, has_sum (λ i, f i x) (g x) :=
+by simp [has_sum, tendsto_pi]
+
+lemma pi.summable {f : ι → ∀ x, π x} : summable f ↔ ∀ x, summable (λ i, f i x) :=
+by simp [summable, pi.has_sum, classical.skolem]
+
+lemma tsum_apply [∀ x, t2_space (π x)] {f : ι → ∀ x, π x}{x : α} (hf : summable f) :
+  (∑' i, f i) x = ∑' i, f i x :=
+(pi.has_sum.mp hf.has_sum x).tsum_eq.symm
+
+end pi
+
 section topological_group
 variables [add_comm_group α] [topological_space α] [topological_add_group α]
 variables {f g : β → α} {a a₁ a₂ : α}

src/topology/algebra/ordered.lean

@@ -120,9 +120,12 @@ section preorder
 variables [topological_space α] [preorder α] [t : order_closed_topology α]
 include t
 
+lemma is_closed_le_prod : is_closed {p : α × α | p.1 ≤ p.2} :=
+t.is_closed_le'
+
 lemma is_closed_le [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
   is_closed {b | f b ≤ g b} :=
-continuous_iff_is_closed.mp (hf.prod_mk hg) _ t.is_closed_le'
+continuous_iff_is_closed.mp (hf.prod_mk hg) _ is_closed_le_prod
 
 lemma is_closed_le' (a : α) : is_closed {b | b ≤ a} :=
 is_closed_le continuous_id continuous_const
@@ -249,6 +252,10 @@ end partial_order
 section linear_order
 variables [topological_space α] [linear_order α] [order_closed_topology α]
 
+lemma is_open_lt_prod : is_open {p : α × α | p.1 < p.2} :=
+by { simp_rw [← is_closed_compl_iff, compl_set_of, not_lt],
+     exact is_closed_le continuous_snd continuous_fst }
+
 lemma is_open_lt [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
   is_open {b | f b < g b} :=
 by simp [lt_iff_not_ge, -not_le]; exact is_closed_le hg hf

src/topology/constructions.lean

@@ -601,6 +601,10 @@ lemma nhds_pi [t : ∀i, topological_space (π i)] {a : Πi, π i} :
 calc 𝓝 a = (⨅i, @nhds _ (@topological_space.induced _ _ (λx:Πi, π i, x i) (t i)) a) : nhds_infi
   ... = (⨅i, comap (λx, x i) (𝓝 (a i))) : by simp [nhds_induced]
 
+lemma tendsto_pi [t : ∀i, topological_space (π i)] {f : α → Πi, π i} {g : Πi, π i} {u : filter α} :
+  tendsto f u (𝓝 g) ↔ ∀ x, tendsto (λ i, f i x) u (𝓝 (g x)) :=
+by simp [nhds_pi, filter.tendsto_comap_iff]
+
 lemma is_open_set_pi [∀a, topological_space (π a)] {i : set ι} {s : Πa, set (π a)}
   (hi : finite i) (hs : ∀a∈i, is_open (s a)) : is_open (pi i s) :=
 by rw [pi_def]; exact (is_open_bInter hi $ assume a ha, continuous_apply a _ $ hs a ha)

src/topology/instances/ennreal.lean

@@ -584,6 +584,10 @@ lemma summable_to_nnreal_of_tsum_ne_top {α : Type*} {f : α → ennreal} (hf :
   summable (ennreal.to_nnreal ∘ f) :=
 by simpa only [←tsum_coe_ne_top_iff_summable, to_nnreal_apply_of_tsum_ne_top hf] using hf
 
+protected lemma tsum_apply {ι α : Type*} {f : ι → α → ennreal} {x : α} :
+  (∑' i, f i) x = ∑' i, f i x :=
+tsum_apply $ pi.summable.mpr $ λ _, ennreal.summable
+
 end tsum
 
 end ennreal

src/topology/list.lean

@@ -5,17 +5,17 @@ Authors: Johannes Hölzl
 
 Topology on lists and vectors.
 -/
-import topology.constructions
+import topology.constructions topology.algebra.group
 
 open topological_space set filter
 open_locale topological_space filter
 
-variables {α : Type*} {β : Type*}
+variables {α : Type*} {β : Type*} [topological_space α] [topological_space β]
 
-instance [topological_space α] : topological_space (list α) :=
+instance : topological_space (list α) :=
 topological_space.mk_of_nhds (traverse nhds)
 
-lemma nhds_list [topological_space α] (as : list α) : 𝓝 as = traverse 𝓝 as :=
+lemma nhds_list (as : list α) : 𝓝 as = traverse 𝓝 as :=
 begin
   refine nhds_mk_of_nhds _ _ _ _,
   { assume l, induction l,
@@ -48,24 +48,23 @@ begin
       exact mem_traverse_sets _ _ (this.imp $ assume a s ⟨hs, ha⟩, mem_nhds_sets hs ha) } }
 end
 
-lemma nhds_nil [topological_space α] : 𝓝 ([] : list α) = pure [] :=
+lemma nhds_nil : 𝓝 ([] : list α) = pure [] :=
 by rw [nhds_list, list.traverse_nil _]; apply_instance
 
-lemma nhds_cons [topological_space α] (a : α) (l : list α) :
+lemma nhds_cons (a : α) (l : list α) :
   𝓝 (a :: l) = list.cons <$> 𝓝 a <*> 𝓝 l  :=
 by rw [nhds_list, list.traverse_cons _, ← nhds_list]; apply_instance
 
-namespace list
-variables [topological_space α] [topological_space β]
-
-lemma tendsto_cons' {a : α} {l : list α} :
+lemma list.tendsto_cons {a : α} {l : list α} :
   tendsto (λp:α×list α, list.cons p.1 p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (a :: l)) :=
 by rw [nhds_cons, tendsto, map_prod]; exact le_refl _
 
-lemma tendsto_cons {α : Type*} {f : α → β} {g : α → list β}
+lemma filter.tendsto.cons {α : Type*} {f : α → β} {g : α → list β}
   {a : _root_.filter α} {b : β} {l : list β} (hf : tendsto f a (𝓝 b)) (hg : tendsto g a (𝓝 l)) :
   tendsto (λa, list.cons (f a) (g a)) a (𝓝 (b :: l)) :=
-tendsto_cons'.comp (tendsto.prod_mk hf hg)
+list.tendsto_cons.comp (tendsto.prod_mk hf hg)
+
+namespace list
 
 lemma tendsto_cons_iff {β : Type*} {f : list α → β} {b : _root_.filter β} {a : α} {l : list α} :
   tendsto f (𝓝 (a :: l)) b ↔ tendsto (λp:α×list α, f (p.1 :: p.2)) (𝓝 a ×ᶠ 𝓝 l) b :=
@@ -77,6 +76,9 @@ begin
 end,
 by rw [this, filter.tendsto_map'_iff]
 
+lemma continuous_cons : continuous (λ x : α × list α, (x.1 :: x.2 : list α)) :=
+continuous_iff_continuous_at.mpr $ λ ⟨x, y⟩, continuous_at_fst.cons continuous_at_snd
+
 lemma tendsto_nhds {β : Type*} {f : list α → β} {r : list α → _root_.filter β}
   (h_nil : tendsto f (pure []) (r []))
   (h_cons : ∀l a, tendsto f (𝓝 l) (r l) → tendsto (λp:α×list α, f (p.1 :: p.2)) (𝓝 a ×ᶠ 𝓝 l) (r (a::l))) :
@@ -98,7 +100,7 @@ end
 
 lemma tendsto_insert_nth' {a : α} : ∀{n : ℕ} {l : list α},
   tendsto (λp:α×list α, insert_nth n p.1 p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (insert_nth n a l))
-| 0     l  := tendsto_cons'
+| 0     l  := tendsto_cons
 | (n+1) [] :=
   suffices tendsto (λa, []) (𝓝 a) (𝓝 ([] : list α)),
     by simpa [nhds_nil, tendsto, map_prod, (∘), insert_nth],
@@ -113,12 +115,11 @@ lemma tendsto_insert_nth' {a : α} : ∀{n : ℕ} {l : list α},
   end,
   begin
     rw [this, tendsto_map'_iff],
-    exact tendsto_cons
-      (tendsto_fst.comp tendsto_snd)
-      ((@tendsto_insert_nth' n l).comp (tendsto.prod_mk tendsto_fst (tendsto_snd.comp tendsto_snd)))
+    exact (tendsto_fst.comp tendsto_snd).cons
+      ((@tendsto_insert_nth' n l).comp $ tendsto_fst.prod_mk $ tendsto_snd.comp tendsto_snd)
   end
 
-lemma tendsto_insert_nth {β : Type*} {n : ℕ} {a : α} {l : list α} {f : β → α} {g : β → list α}
+lemma tendsto_insert_nth {β} {n : ℕ} {a : α} {l : list α} {f : β → α} {g : β → list α}
   {b : _root_.filter β} (hf : tendsto f b (𝓝 a)) (hg : tendsto g b (𝓝 l)) :
   tendsto (λb:β, insert_nth n (f b) (g b)) b (𝓝 (insert_nth n a l)) :=
 tendsto_insert_nth'.comp (tendsto.prod_mk hf hg)
@@ -135,27 +136,42 @@ lemma tendsto_remove_nth : ∀{n : ℕ} {l : list α},
   begin
     rw [tendsto_cons_iff],
     dsimp [remove_nth],
-    exact tendsto_cons tendsto_fst ((@tendsto_remove_nth n l).comp tendsto_snd)
+    exact tendsto_fst.cons ((@tendsto_remove_nth n l).comp tendsto_snd)
   end
 
 lemma continuous_remove_nth {n : ℕ} : continuous (λl : list α, remove_nth l n) :=
 continuous_iff_continuous_at.mpr $ assume a, tendsto_remove_nth
 
+@[to_additive]
+lemma tendsto_prod [monoid α] [has_continuous_mul α] {l : list α} :
+  tendsto list.prod (𝓝 l) (𝓝 l.prod) :=
+begin
+  induction l with x l ih, { simp [nhds_nil, mem_of_nhds, tendsto_pure_left] {contextual := tt} },
+  simp_rw [tendsto_cons_iff, prod_cons],
+  have := continuous_iff_continuous_at.mp continuous_mul (x, l.prod),
+  rw [continuous_at, nhds_prod_eq] at this,
+  exact this.comp (tendsto_id.prod_map ih)
+end
+
+@[to_additive]
+lemma continuous_prod [monoid α] [has_continuous_mul α] : continuous (prod : list α → α) :=
+continuous_iff_continuous_at.mpr $ λ l, tendsto_prod
+
 end list
 
 namespace vector
 open list
 
-instance (n : ℕ) [topological_space α] : topological_space (vector α n) :=
+instance (n : ℕ) : topological_space (vector α n) :=
 by unfold vector; apply_instance
 
-lemma tendsto_cons [topological_space α] {n : ℕ} {a : α} {l : vector α n}:
+lemma tendsto_cons {n : ℕ} {a : α} {l : vector α n}:
   tendsto (λp:α×vector α n, vector.cons p.1 p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (a :: l)) :=
 by { simp [tendsto_subtype_rng, ←subtype.val_eq_coe, cons_val],
-  exact tendsto_cons tendsto_fst (tendsto.comp continuous_at_subtype_coe tendsto_snd) }
+  exact tendsto_fst.cons (tendsto.comp continuous_at_subtype_coe tendsto_snd) }
 
 lemma tendsto_insert_nth
-  [topological_space α] {n : ℕ} {i : fin (n+1)} {a:α} :
+  {n : ℕ} {i : fin (n+1)} {a:α} :
   ∀{l:vector α n}, tendsto (λp:α×vector α n, insert_nth p.1 i p.2)
     (𝓝 a ×ᶠ 𝓝 l) (𝓝 (insert_nth a i l))
 | ⟨l, hl⟩ :=
@@ -165,17 +181,17 @@ begin
   exact list.tendsto_insert_nth tendsto_fst (tendsto.comp continuous_at_subtype_coe tendsto_snd : _)
 end
 
-lemma continuous_insert_nth' [topological_space α] {n : ℕ} {i : fin (n+1)} :
+lemma continuous_insert_nth' {n : ℕ} {i : fin (n+1)} :
   continuous (λp:α×vector α n, insert_nth p.1 i p.2) :=
 continuous_iff_continuous_at.mpr $ assume ⟨a, l⟩,
   by rw [continuous_at, nhds_prod_eq]; exact tendsto_insert_nth
 
-lemma continuous_insert_nth [topological_space α] [topological_space β] {n : ℕ} {i : fin (n+1)}
+lemma continuous_insert_nth {n : ℕ} {i : fin (n+1)}
   {f : β → α} {g : β → vector α n} (hf : continuous f) (hg : continuous g) :
   continuous (λb, insert_nth (f b) i (g b)) :=
 continuous_insert_nth'.comp (continuous.prod_mk hf hg)
 
-lemma continuous_at_remove_nth [topological_space α] {n : ℕ} {i : fin (n+1)} :
+lemma continuous_at_remove_nth {n : ℕ} {i : fin (n+1)} :
   ∀{l:vector α (n+1)}, continuous_at (remove_nth i) l
 | ⟨l, hl⟩ :=
 --  ∀{l:vector α (n+1)}, tendsto (remove_nth i) (𝓝 l) (𝓝 (remove_nth i l))
@@ -186,7 +202,7 @@ begin
   exact tendsto.comp list.tendsto_remove_nth continuous_at_subtype_coe,
 end
 
-lemma continuous_remove_nth [topological_space α] {n : ℕ} {i : fin (n+1)} :
+lemma continuous_remove_nth {n : ℕ} {i : fin (n+1)} :
   continuous (remove_nth i : vector α (n+1) → vector α n) :=
 continuous_iff_continuous_at.mpr $ assume ⟨a, l⟩, continuous_at_remove_nth
 

src/topology/metric_space/hausdorff_distance.lean

@@ -25,7 +25,7 @@ This files introduces:
 `Hausdorff_dist`.
 -/
 noncomputable theory
-open_locale classical
+open_locale classical nnreal
 universes u v w
 
 open classical set function topological_space filter
@@ -36,6 +36,8 @@ section inf_edist
 open_locale ennreal
 variables {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {x y : α} {s t : set α} {Φ : α → β}
 
+/-! ### Distance of a point to a set as a function into `ennreal`. -/
+
 /-- The minimal edistance of a point to a set -/
 def inf_edist (x : α) (s : set α) : ennreal := Inf ((edist x) '' s)
 
@@ -142,6 +144,8 @@ end
 
 end inf_edist --section
 
+/-! ### The Hausdorff distance as a function into `ennreal`. -/
+
 /-- The Hausdorff edistance between two sets is the smallest `r` such that each set
 is contained in the `r`-neighborhood of the other one -/
 def Hausdorff_edist {α : Type u} [emetric_space α] (s t : set α) : ennreal :=
@@ -374,17 +378,19 @@ end Hausdorff_edist -- section
 end emetric --namespace
 
 
-/-Now, we turn to the same notions in metric spaces. To avoid the difficulties related to
-Inf and Sup on ℝ (which is only conditionnally complete), we use the notions in ennreal formulated
-in terms of the edistance, and coerce them to ℝ. Then their properties follow readily from the
-corresponding properties in ennreal, modulo some tedious rewriting of inequalities from one to the
-other -/
+/-! Now, we turn to the same notions in metric spaces. To avoid the difficulties related to
+`Inf` and `Sup` on `ℝ` (which is only conditionally complete), we use the notions in `ennreal`
+formulated in terms of the edistance, and coerce them to `ℝ`.
+Then their properties follow readily from the corresponding properties in `ennreal`,
+modulo some tedious rewriting of inequalities from one to the other. -/
 
 namespace metric
 section
 variables {α : Type u} {β : Type v} [metric_space α] [metric_space β] {s t u : set α} {x y : α} {Φ : α → β}
 open emetric
 
+/-! ### Distance of a point to a set as a function into `ℝ`. -/
+
 /-- The minimal distance of a point to a set -/
 def inf_dist (x : α) (s : set α) : ℝ := ennreal.to_real (inf_edist x s)
 
@@ -492,6 +498,27 @@ lemma inf_dist_image (hΦ : isometry Φ) :
   inf_dist (Φ x) (Φ '' t) = inf_dist x t :=
 by simp [inf_dist, inf_edist_image hΦ]
 
+/-! ### Distance of a point to a set as a function into `ℝ≥0`. -/
+
+/-- The minimal distance of a point to a set as a `nnreal` -/
+def inf_nndist (x : α) (s : set α) : ℝ≥0 := ennreal.to_nnreal (inf_edist x s)
+@[simp] lemma coe_inf_nndist : (inf_nndist x s : ℝ) = inf_dist x s := rfl
+
+/-- The minimal distance to a set (as `nnreal`) is Lipschitz in point with constant 1 -/
+lemma lipschitz_inf_nndist_pt (s : set α) : lipschitz_with 1 (λx, inf_nndist x s) :=
+lipschitz_with.of_le_add $ λ x y, inf_dist_le_inf_dist_add_dist
+
+/-- The minimal distance to a set (as `nnreal`) is uniformly continuous in point -/
+lemma uniform_continuous_inf_nndist_pt (s : set α) :
+  uniform_continuous (λx, inf_nndist x s) :=
+(lipschitz_inf_nndist_pt s).uniform_continuous
+
+/-- The minimal distance to a set (as `nnreal`) is continuous in point -/
+lemma continuous_inf_nndist_pt (s : set α) : continuous (λx, inf_nndist x s) :=
+(uniform_continuous_inf_nndist_pt s).continuous
+
+/-! ### The Hausdorff distance as a function into `ℝ`. -/
+
 /-- The Hausdorff distance between two sets is the smallest nonnegative `r` such that each set is
 included in the `r`-neighborhood of the other. If there is no such `r`, it is defined to
 be `0`, arbitrarily -/