feat(topology/bases): a family of nonempty disjoint open sets is coun…

…table in a separable space (#9557)

Together with unrelated small lemmas on balls and on `pairwise_on`.

src/analysis/normed_space/riesz_lemma.lean

@@ -35,7 +35,7 @@ begin
   have hFn : (F : set E).nonempty, from ⟨_, F.zero_mem⟩,
   have hdp : 0 < d,
     from lt_of_le_of_ne metric.inf_dist_nonneg (λ heq, hx
-    ((metric.mem_iff_inf_dist_zero_of_closed hFc hFn).2 heq.symm)),
+    ((hFc.mem_iff_inf_dist_zero hFn).2 heq.symm)),
   let r' := max r 2⁻¹,
   have hr' : r' < 1, by { simp [r', hr], norm_num },
   have hlt : 0 < r' := lt_of_lt_of_le (by norm_num) (le_max_right r 2⁻¹),

src/data/real/ennreal.lean

@@ -896,6 +896,28 @@ begin
   exact real.to_nnreal_sum_of_nonneg hf,
 end
 
+theorem sum_lt_sum_of_nonempty {s : finset α} (hs : s.nonempty)
+  {f g : α → ℝ≥0∞} (Hlt : ∀ i ∈ s, f i < g i) :
+  ∑ i in s, f i < ∑ i in s, g i :=
+begin
+  classical,
+  induction s using finset.induction_on with a s as IH,
+  { exact (finset.not_nonempty_empty hs).elim },
+  { rcases finset.eq_empty_or_nonempty s with rfl|h's,
+    { simp [Hlt _ (finset.mem_singleton_self _)] },
+    { simp only [as, finset.sum_insert, not_false_iff],
+      exact ennreal.add_lt_add (Hlt _ (finset.mem_insert_self _ _))
+        (IH h's (λ i hi, Hlt _ (finset.mem_insert_of_mem hi))) } }
+end
+
+theorem exists_le_of_sum_le {s : finset α} (hs : s.nonempty)
+  {f g : α → ℝ≥0∞} (Hle : ∑ i in s, f i ≤ ∑ i in s, g i) :
+  ∃ i ∈ s, f i ≤ g i :=
+begin
+  contrapose! Hle,
+  apply ennreal.sum_lt_sum_of_nonempty hs Hle,
+end
+
 end sum
 
 section interval

src/data/set/basic.lean

@@ -2019,6 +2019,11 @@ lemma pairwise_on_pair_of_symmetric {r : α → α → Prop} {x y : α} (hr : sy
   pairwise_on {x, y} r ↔ (x ≠ y → r x y) :=
 by simp [pairwise_on_insert_of_symmetric hr]
 
+lemma pairwise_on_disjoint_on_mono {s : set α} {f g : α → set β}
+  (h : s.pairwise_on (disjoint on f)) (h' : ∀ x ∈ s, g x ⊆ f x) :
+  s.pairwise_on (disjoint on g) :=
+λ i hi j hj hij, disjoint.mono (h' i hi) (h' j hj) (h i hi j hj hij)
+
 end set
 
 open set

src/data/set/lattice.lean

@@ -301,6 +301,19 @@ let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂,
     ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂) in
 ⟨x, ⟨z, xf⟩, xa₁, xa₂⟩
 
+lemma pairwise_on_Union {r : α → α → Prop} {f : ι → set α} (h : directed (⊆) f) :
+  (⋃ n, f n).pairwise_on r ↔ (∀ n, (f n).pairwise_on r) :=
+begin
+  split,
+  { assume H n,
+    exact pairwise_on.mono (subset_Union _ _) H },
+  { assume H i hi j hj hij,
+    rcases mem_Union.1 hi with ⟨m, hm⟩,
+    rcases mem_Union.1 hj with ⟨n, hn⟩,
+    rcases h m n with ⟨p, mp, np⟩,
+    exact H p i (mp hm) j (np hn) hij }
+end
+
 lemma Union_inter_subset {ι α} {s t : ι → set α} : (⋃ i, s i ∩ t i) ⊆ (⋃ i, s i) ∩ (⋃ i, t i) :=
 by { rintro x ⟨_, ⟨i, rfl⟩, xs, xt⟩, exact ⟨⟨_, ⟨i, rfl⟩, xs⟩, _, ⟨i, rfl⟩, xt⟩ }
 

src/measure_theory/constructions/borel_space.lean

@@ -1453,7 +1453,7 @@ begin
     rw [tendsto_pi], rw [tendsto_pi] at lim, intro x,
     exact ((continuous_inf_nndist_pt s).tendsto (g x)).comp (lim x) },
   have h4s : g ⁻¹' s = (λ x, inf_nndist (g x) s) ⁻¹' {0},
-  { ext x, simp [h1s, ← mem_iff_inf_dist_zero_of_closed h1s h2s, ← nnreal.coe_eq_zero] },
+  { ext x, simp [h1s, ← h1s.mem_iff_inf_dist_zero h2s, ← nnreal.coe_eq_zero] },
   rw [h4s], exact this (measurable_set_singleton 0),
 end
 

src/topology/bases.lean

@@ -261,6 +261,47 @@ def dense_seq [separable_space α] [nonempty α] : ℕ → α := classical.some
 @[simp] lemma dense_range_dense_seq [separable_space α] [nonempty α] :
   dense_range (dense_seq α) := classical.some_spec (exists_dense_seq α)
 
+variable {α}
+
+/-- In a separable space, a family of nonempty disjoint open sets is countable. -/
+lemma countable_of_is_open_of_disjoint [separable_space α] {β : Type*}
+  (s : β → set α) {a : set β} (ha : ∀ i ∈ a, is_open (s i)) (h'a : ∀ i ∈ a, (s i).nonempty)
+  (h : a.pairwise_on (disjoint on s)) :
+  countable a :=
+begin
+  rcases eq_empty_or_nonempty a with rfl|H, { exact countable_empty },
+  haveI : inhabited α,
+  { choose i ia using H,
+    choose y hy using h'a i ia,
+    exact ⟨y⟩ },
+  rcases exists_countable_dense α with ⟨u, u_count, u_dense⟩,
+  have : ∀ i, i ∈ a → ∃ y, y ∈ s i ∩ u :=
+    λ i hi, dense_iff_inter_open.1 u_dense (s i) (ha i hi) (h'a i hi),
+  choose! f hf using this,
+  have f_inj : inj_on f a,
+  { assume i hi j hj hij,
+    have : ¬disjoint (s i) (s j),
+    { rw not_disjoint_iff_nonempty_inter,
+      refine ⟨f i, (hf i hi).1, _⟩,
+      rw hij,
+      exact (hf j hj).1 },
+    contrapose! this,
+    exact h i hi j hj this },
+  apply countable_of_injective_of_countable_image f_inj,
+  apply u_count.mono _,
+  exact image_subset_iff.2 (λ i hi, (hf i hi).2)
+end
+
+/-- In a separable space, a family of disjoint sets with nonempty interiors is countable. -/
+lemma countable_of_nonempty_interior_of_disjoint [separable_space α] {β : Type*} (s : β → set α)
+  {a : set β} (ha : ∀ i ∈ a, (interior (s i)).nonempty) (h : a.pairwise_on (disjoint on s)) :
+  countable a :=
+begin
+  have : a.pairwise_on (disjoint on (λ i, interior (s i))) :=
+    pairwise_on_disjoint_on_mono h (λ i hi, interior_subset),
+  exact countable_of_is_open_of_disjoint (λ i, interior (s i)) (λ i hi, is_open_interior) ha this
+end
+
 end topological_space
 
 open topological_space

src/topology/metric_space/gromov_hausdorff.lean

@@ -404,7 +404,7 @@ instance : metric_space GH_space :=
     have : range Φ = range Ψ,
     { have hΦ : is_compact (range Φ) := is_compact_range Φisom.continuous,
       have hΨ : is_compact (range Ψ) := is_compact_range Ψisom.continuous,
-      apply (Hausdorff_dist_zero_iff_eq_of_closed _ _ _).1 (DΦΨ.symm),
+      apply (is_closed.Hausdorff_dist_zero_iff_eq _ _ _).1 (DΦΨ.symm),
       { exact hΦ.is_closed },
       { exact hΨ.is_closed },
       { exact Hausdorff_edist_ne_top_of_nonempty_of_bounded (range_nonempty _)

src/topology/metric_space/hausdorff_distance.lean

@@ -116,6 +116,17 @@ begin
   exact h.closure_eq
 end
 
+lemma disjoint_closed_ball_of_lt_inf_edist {r : ℝ≥0∞} (h : r < inf_edist x s) :
+  disjoint (closed_ball x r) s :=
+begin
+  rw disjoint_left,
+  assume y hy h'y,
+  apply lt_irrefl (inf_edist x s),
+  calc inf_edist x s ≤ edist x y : inf_edist_le_edist_of_mem h'y
+  ... ≤ r : by rwa [mem_closed_ball, edist_comm] at hy
+  ... < inf_edist x s : h
+end
+
 /-- The infimum edistance is invariant under isometries -/
 lemma inf_edist_image (hΦ : isometry Φ) :
   inf_edist (Φ x) (Φ '' t) = inf_edist x t :=
@@ -433,6 +444,17 @@ begin
     { simp [ennreal.add_eq_top, inf_edist_ne_top hs, edist_ne_top] }}
 end
 
+lemma disjoint_closed_ball_of_lt_inf_dist {r : ℝ} (h : r < inf_dist x s) :
+  disjoint (closed_ball x r) s :=
+begin
+  rw disjoint_left,
+  assume y hy h'y,
+  apply lt_irrefl (inf_dist x s),
+  calc inf_dist x s ≤ dist x y : inf_dist_le_dist_of_mem h'y
+  ... ≤ r : by rwa [mem_closed_ball, dist_comm] at hy
+  ... < inf_dist x s : h
+end
+
 variable (s)
 
 /-- The minimal distance to a set is Lipschitz in point with constant 1 -/
@@ -460,13 +482,22 @@ lemma mem_closure_iff_inf_dist_zero (h : s.nonempty) : x ∈ closure s ↔ inf_d
 by simp [mem_closure_iff_inf_edist_zero, inf_dist, ennreal.to_real_eq_zero_iff, inf_edist_ne_top h]
 
 /-- Given a closed set `s`, a point belongs to `s` iff its infimum distance to this set vanishes -/
-lemma mem_iff_inf_dist_zero_of_closed (h : is_closed s) (hs : s.nonempty) :
+lemma _root_.is_closed.mem_iff_inf_dist_zero (h : is_closed s) (hs : s.nonempty) :
   x ∈ s ↔ inf_dist x s = 0 :=
 begin
   have := @mem_closure_iff_inf_dist_zero _ _ s x hs,
   rwa h.closure_eq at this
 end
 
+/-- Given a closed set `s`, a point belongs to `s` iff its infimum distance to this set vanishes -/
+lemma _root_.is_closed.not_mem_iff_inf_dist_pos (h : is_closed s) (hs : s.nonempty) :
+  x ∉ s ↔ 0 < inf_dist x s :=
+begin
+  rw ← not_iff_not,
+  push_neg,
+  simp [h.mem_iff_inf_dist_zero hs, le_antisymm_iff, inf_dist_nonneg],
+end
+
 /-- The infimum distance is invariant under isometries -/
 lemma inf_dist_image (hΦ : isometry Φ) :
   inf_dist (Φ x) (Φ '' t) = inf_dist x t :=
@@ -706,7 +737,7 @@ by simp [Hausdorff_edist_zero_iff_closure_eq_closure.symm, Hausdorff_dist,
          ennreal.to_real_eq_zero_iff, fin]
 
 /-- Two closed sets are at zero Hausdorff distance if and only if they coincide -/
-lemma Hausdorff_dist_zero_iff_eq_of_closed (hs : is_closed s) (ht : is_closed t)
+lemma _root_.is_closed.Hausdorff_dist_zero_iff_eq (hs : is_closed s) (ht : is_closed t)
   (fin : Hausdorff_edist s t ≠ ⊤) : Hausdorff_dist s t = 0 ↔ s = t :=
 by simp [(Hausdorff_edist_zero_iff_eq_of_closed hs ht).symm, Hausdorff_dist,
          ennreal.to_real_eq_zero_iff, fin]