feat(order/filter/*): a family of pairwise disjoint filters has a fam…

…ily of pairwise disjoint members (#16504)

src/order/filter/bases.lean

@@ -564,6 +564,31 @@ lemma has_basis.disjoint_iff (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
 not_iff_not.mp $ by simp only [disjoint_iff, ← ne.def, ← ne_bot_iff, hl.inf_basis_ne_bot_iff hl',
   not_exists, bot_eq_empty, ne_empty_iff_nonempty, inf_eq_inter]
 
+lemma _root_.disjoint.exists_mem_filter_basis (h : disjoint l l') (hl : l.has_basis p s)
+  (hl' : l'.has_basis p' s') :
+  ∃ i (hi : p i) i' (hi' : p' i'), disjoint (s i) (s' i') :=
+(hl.disjoint_iff hl').1 h
+
+lemma _root_.pairwise.exists_mem_filter_basis_of_disjoint {I : Type*} [finite I]
+  {l : I → filter α} {ι : I → Sort*} {p : Π i, ι i → Prop} {s : Π i, ι i → set α}
+  (hd : pairwise (disjoint on l)) (h : ∀ i, (l i).has_basis (p i) (s i)) :
+  ∃ ind : Π i, ι i, (∀ i, p i (ind i)) ∧ pairwise (disjoint on λ i, s i (ind i)) :=
+begin
+  rcases hd.exists_mem_filter_of_disjoint with ⟨t, htl, hd⟩,
+  choose ind hp ht using λ i, (h i).mem_iff.1 (htl i),
+  exact ⟨ind, hp, hd.mono $ λ i j hij, hij.mono (ht _) (ht _)⟩
+end
+
+lemma _root_.set.pairwise_disjoint.exists_mem_filter_basis {I : Type*} {l : I → filter α}
+  {ι : I → Sort*} {p : Π i, ι i → Prop} {s : Π i, ι i → set α} {S : set I}
+  (hd : S.pairwise_disjoint l) (hS : S.finite) (h : ∀ i, (l i).has_basis (p i) (s i)) :
+  ∃ ind : Π i, ι i, (∀ i, p i (ind i)) ∧ S.pairwise_disjoint (λ i, s i (ind i)) :=
+begin
+  rcases hd.exists_mem_filter hS with ⟨t, htl, hd⟩,
+  choose ind hp ht using λ i, (h i).mem_iff.1 (htl i),
+  exact ⟨ind, hp, hd.mono ht⟩
+end
+
 lemma inf_ne_bot_iff :
   ne_bot (l ⊓ l') ↔ ∀ ⦃s : set α⦄ (hs : s ∈ l) ⦃s'⦄ (hs' : s' ∈ l'), (s ∩ s').nonempty :=
 l.basis_sets.inf_ne_bot_iff

src/order/filter/basic.lean

@@ -630,6 +630,31 @@ lemma inf_eq_bot_iff {f g : filter α} :
   f ⊓ g = ⊥ ↔ ∃ (U ∈ f) (V ∈ g), U ∩ V = ∅ :=
 by simpa only [disjoint_iff] using filter.disjoint_iff
 
+lemma _root_.pairwise.exists_mem_filter_of_disjoint {ι : Type*} [finite ι]
+  {l : ι → filter α} (hd : pairwise (disjoint on l)) :
+  ∃ s : ι → set α, (∀ i, s i ∈ l i) ∧ pairwise (disjoint on s) :=
+begin
+  simp only [pairwise, function.on_fun, filter.disjoint_iff, subtype.exists'] at hd,
+  choose! s t hst using hd,
+  refine ⟨λ i, ⋂ j, s i j ∩ t j i, λ i, _, λ i j hij, _⟩,
+  exacts [Inter_mem.2 (λ j, inter_mem (s i j).2 (t j i).2),
+    (hst i j hij).mono ((Inter_subset _ j).trans (inter_subset_left _ _))
+      ((Inter_subset _ i).trans (inter_subset_right _ _))]
+end
+
+lemma _root_.set.pairwise_disjoint.exists_mem_filter {ι : Type*} {l : ι → filter α} {t : set ι}
+  (hd : t.pairwise_disjoint l) (ht : t.finite) :
+  ∃ s : ι → set α, (∀ i, s i ∈ l i) ∧ t.pairwise_disjoint s :=
+begin
+  casesI ht,
+  obtain ⟨s, hd⟩ : ∃ s : Π i : t, {s : set α // s ∈ l i}, pairwise (disjoint on λ i, (s i : set α)),
+  { rcases (hd.subtype _ _).exists_mem_filter_of_disjoint with ⟨s, hsl, hsd⟩,
+    exact ⟨λ i, ⟨s i, hsl i⟩, hsd⟩ },
+  -- TODO: Lean fails to find `can_lift` instance and fails to use an instance supplied by `letI`
+  rcases @subtype.exists_pi_extension ι (λ i, {s // s ∈ l i}) _ _ s with ⟨s, rfl⟩,
+  exact ⟨λ i, s i, λ i, (s i).2, pairwise.set_of_subtype _ _ hd⟩
+end
+
 /-- There is exactly one filter on an empty type. --/
 instance unique [is_empty α] : unique (filter α) :=
 { default := ⊥, uniq := filter_eq_bot_of_is_empty }

src/topology/separation.lean

@@ -804,6 +804,17 @@ end
 @[simp] lemma disjoint_nhds_nhds [t2_space α] {x y : α} : disjoint (𝓝 x) (𝓝 y) ↔ x ≠ y :=
 ⟨λ hd he, by simpa [he, nhds_ne_bot.ne] using hd, t2_space_iff_disjoint_nhds.mp ‹_› x y⟩
 
+lemma pairwise_disjoint_nhds [t2_space α] : pairwise (disjoint on (𝓝 : α → filter α)) :=
+λ x y, disjoint_nhds_nhds.2
+
+protected lemma set.pairwise_disjoint_nhds [t2_space α] (s : set α) : s.pairwise_disjoint 𝓝 :=
+pairwise_disjoint_nhds.set_pairwise s
+
+/-- Points of a finite set can be separated by open sets from each other. -/
+lemma set.finite.t2_separation [t2_space α] {s : set α} (hs : s.finite) :
+  ∃ U : α → set α, (∀ x, x ∈ U x ∧ is_open (U x)) ∧ s.pairwise_disjoint U :=
+s.pairwise_disjoint_nhds.exists_mem_filter_basis hs nhds_basis_opens
+
 lemma is_open_set_of_disjoint_nhds_nhds :
   is_open {p : α × α | disjoint (𝓝 p.1) (𝓝 p.2)} :=
 begin
@@ -814,37 +825,6 @@ begin
     λ ⟨x', y'⟩ ⟨hx', hy'⟩, disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩
 end
 
-/-- A finite set can be separated by open sets. -/
-lemma t2_separation_finset [t2_space α] (s : finset α) :
-  ∃ f : α → set α, set.pairwise_disjoint ↑s f ∧ ∀ x ∈ s, x ∈ f x ∧ is_open (f x) :=
-finset.induction_on s (by simp) begin
-  rintros t s ht ⟨f, hf, hf'⟩,
-  have hty : ∀ y : s, t ≠ y := by { rintros y rfl, exact ht y.2 },
-  choose u v hu hv htu hxv huv using λ {x} (h : t ≠ x), t2_separation h,
-  refine ⟨λ x, if ht : t = x then ⋂ y : s, u (hty y) else f x ∩ v ht, _, _⟩,
-  { rintros x hx₁ y hy₁ hxy a ⟨hx, hy⟩,
-    rw [finset.mem_coe, finset.mem_insert, eq_comm] at hx₁ hy₁,
-    rcases eq_or_ne t x with rfl | hx₂;
-    rcases eq_or_ne t y with rfl | hy₂,
-    { exact hxy rfl },
-    { simp_rw [dif_pos rfl, mem_Inter] at hx,
-      simp_rw [dif_neg hy₂] at hy,
-      exact huv hy₂ ⟨hx ⟨y, hy₁.resolve_left hy₂⟩, hy.2⟩ },
-    { simp_rw [dif_neg hx₂] at hx,
-      simp_rw [dif_pos rfl, mem_Inter] at hy,
-      exact huv hx₂ ⟨hy ⟨x, hx₁.resolve_left hx₂⟩, hx.2⟩ },
-    { simp_rw [dif_neg hx₂] at hx,
-      simp_rw [dif_neg hy₂] at hy,
-      exact hf (hx₁.resolve_left hx₂) (hy₁.resolve_left hy₂) hxy ⟨hx.1, hy.1⟩ } },
-  { intros x hx,
-    split_ifs with ht,
-    { refine ⟨mem_Inter.2 (λ y, _), is_open_Inter (λ y, hu (hty y))⟩,
-      rw ←ht,
-      exact htu (hty y) },
-    { have hx := hf' x ((finset.mem_insert.1 hx).resolve_left (ne.symm ht)),
-      exact ⟨⟨hx.1, hxv ht⟩, is_open.inter hx.2 (hv ht)⟩ } }
-end
-
 @[priority 100] -- see Note [lower instance priority]
 instance t2_space.t1_space [t2_space α] : t1_space α :=
 t1_space_iff_disjoint_pure_nhds.mpr $ λ x y hne, (disjoint_nhds_nhds.2 hne).mono_left $