feat(topology/separation): add subtype.t1_space and `subtype.regula…

…r` (#2667)

Also simplify the proof of `exists_open_singleton_of_fintype`

src/data/finset.lean

@@ -806,6 +806,10 @@ def filter (p : α → Prop) [decidable_pred p] (s : finset α) : finset α :=
 
 @[simp] theorem filter_subset (s : finset α) : s.filter p ⊆ s := filter_subset _
 
+theorem filter_ssubset {s : finset α} : s.filter p ⊂ s ↔ ∃ x ∈ s, ¬ p x :=
+⟨λ h, let ⟨x, hs, hp⟩ := set.exists_of_ssubset h in ⟨x, hs, mt (λ hp, mem_filter.2 ⟨hs, hp⟩) hp⟩,
+  λ ⟨x, hs, hp⟩, ⟨s.filter_subset, λ h, hp (mem_filter.1 (h hs)).2⟩⟩
+
 theorem filter_filter (s : finset α) :
   (s.filter p).filter q = s.filter (λa, p a ∧ q a) :=
 ext.2 $ assume a, by simp only [mem_filter, and_comm, and.left_comm]

src/topology/separation.lean

@@ -21,96 +21,41 @@ section separation
 class t0_space (α : Type u) [topological_space α] : Prop :=
 (t0 : ∀ x y, x ≠ y → ∃ U:set α, is_open U ∧ (xor (x ∈ U) (y ∈ U)))
 
+theorem exists_open_singleton_of_open_finset [t0_space α] (s : finset α) (sne : s.nonempty)
+  (hso : is_open (↑s : set α)) :
+  ∃ x ∈ s, is_open ({x} : set α):=
+begin
+  induction s using finset.strong_induction_on with s ihs,
+  by_cases hs : set.subsingleton (↑s : set α),
+  { rcases sne with ⟨x, hx⟩,
+    refine ⟨x, hx, _⟩,
+    have : (↑s : set α) = {x}, from hs.eq_singleton_of_mem hx,
+    rwa this at hso },
+  { dunfold set.subsingleton at hs,
+    push_neg at hs,
+    rcases hs with ⟨x, hx, y, hy, hxy⟩,
+    rcases t0_space.t0 x y hxy with ⟨U, hU, hxyU⟩,
+    wlog H : x ∈ U ∧ y ∉ U := hxyU using [x y, y x],
+    obtain ⟨z, hzs, hz⟩ : ∃ z ∈ s.filter (λ z, z ∈ U), is_open ({z} : set α),
+    { refine ihs _ (finset.filter_ssubset.2 ⟨y, hy, H.2⟩) ⟨x, finset.mem_filter.2 ⟨hx, H.1⟩⟩ _,
+      rw [finset.coe_filter],
+      exact is_open_inter hso hU },
+    exact ⟨z, (finset.mem_filter.1 hzs).1, hz⟩ }
+end
+
 theorem exists_open_singleton_of_fintype [t0_space α] [f : fintype α] [ha : nonempty α] :
   ∃ x:α, is_open ({x}:set α) :=
-have H : ∀ (T : finset α), T ≠ ∅ → ∃ x ∈ T, ∃ u, is_open u ∧ {x} = {y | y ∈ T} ∩ u :=
-begin
-  classical,
-  intro T,
-  apply finset.case_strong_induction_on T,
-  { intro h, exact (h rfl).elim },
-  { intros x S hxS ih h,
-    by_cases hs : S = ∅,
-    { existsi [x, finset.mem_insert_self x S, univ, is_open_univ],
-      rw [hs, inter_univ], refl },
-    { rcases ih S (finset.subset.refl S) hs with ⟨y, hy, V, hv1, hv2⟩,
-      by_cases hxV : x ∈ V,
-      { cases t0_space.t0 x y (λ hxy, hxS $ by rwa hxy) with U hu,
-        rcases hu with ⟨hu1, ⟨hu2, hu3⟩ | ⟨hu2, hu3⟩⟩,
-        { existsi [x, finset.mem_insert_self x S, U ∩ V, is_open_inter hu1 hv1],
-          apply set.ext,
-          intro z,
-          split,
-          { intro hzx,
-            rw set.mem_singleton_iff at hzx,
-            rw hzx,
-            exact ⟨finset.mem_insert_self x S, ⟨hu2, hxV⟩⟩ },
-          { intro hz,
-            rw set.mem_singleton_iff,
-            rcases hz with ⟨hz1, hz2, hz3⟩,
-            cases finset.mem_insert.1 hz1 with hz4 hz4,
-            { exact hz4 },
-            { have h1 : z ∈ {y : α | y ∈ S} ∩ V,
-              { exact ⟨hz4, hz3⟩ },
-              rw ← hv2 at h1,
-              rw set.mem_singleton_iff at h1,
-              rw h1 at hz2,
-              exact (hu3 hz2).elim } } },
-        { existsi [y, finset.mem_insert_of_mem hy, U ∩ V, is_open_inter hu1 hv1],
-          apply set.ext,
-          intro z,
-          split,
-          { intro hz,
-            rw set.mem_singleton_iff at hz,
-            rw hz,
-            refine ⟨finset.mem_insert_of_mem hy, hu2, _⟩,
-            have h1 : y ∈ {y} := set.mem_singleton y,
-            rw hv2 at h1,
-            exact h1.2 },
-          { intro hz,
-            rw set.mem_singleton_iff,
-            cases hz with hz1 hz2,
-            cases finset.mem_insert.1 hz1 with hz3 hz3,
-            { rw hz3 at hz2,
-              exact (hu3 hz2.1).elim },
-            { have h1 : z ∈ {y : α | y ∈ S} ∩ V := ⟨hz3, hz2.2⟩,
-              rw ← hv2 at h1,
-              rw set.mem_singleton_iff at h1,
-              exact h1 } } } },
-      { existsi [y, finset.mem_insert_of_mem hy, V, hv1],
-        apply set.ext,
-        intro z,
-        split,
-        { intro hz,
-          rw set.mem_singleton_iff at hz,
-          rw hz,
-          split,
-          { exact finset.mem_insert_of_mem hy },
-          { have h1 : y ∈ {y} := set.mem_singleton y,
-            rw hv2 at h1,
-            exact h1.2 } },
-        { intro hz,
-          rw hv2,
-          cases hz with hz1 hz2,
-          cases finset.mem_insert.1 hz1 with hz3 hz3,
-          { rw hz3 at hz2,
-            exact (hxV hz2).elim },
-          { exact ⟨hz3, hz2⟩ } } } } }
-end,
 begin
-  apply nonempty.elim ha, intro x,
-  specialize H finset.univ (finset.ne_empty_of_mem $ finset.mem_univ x),
-  rcases H with ⟨y, hyf, U, hu1, hu2⟩,
-  existsi y,
-  have h1 : {y : α | y ∈ finset.univ} = (univ : set α),
-  { exact set.eq_univ_of_forall (λ x : α,
-      by rw mem_set_of_eq; exact finset.mem_univ x) },
-  rw h1 at hu2,
-  rw set.univ_inter at hu2,
-  rw hu2,
-  exact hu1
+  refine ha.elim (λ x, _),
+  have : is_open (↑(finset.univ : finset α) : set α), { simp },
+  rcases exists_open_singleton_of_open_finset _ ⟨x, finset.mem_univ x⟩ this with ⟨x, _, hx⟩,
+  exact ⟨x, hx⟩
 end
 
+instance subtype.t0_space [t0_space α] {p : α → Prop} : t0_space (subtype p) :=
+⟨λ x y hxy, let ⟨U, hU, hxyU⟩ := t0_space.t0 (x:α) y ((not_congr subtype.coe_ext).1 hxy) in
+  ⟨(coe : subtype p → α) ⁻¹' U, is_open_induced hU, hxyU⟩⟩
+
 /-- A T₁ space, also known as a Fréchet space, is a topological space
   where every singleton set is closed. Equivalently, for every pair
   `x ≠ y`, there is an open set containing `x` and not `y`. -/
@@ -123,6 +68,11 @@ t1_space.t1 x
 lemma is_open_ne [t1_space α] {x : α} : is_open {y | y ≠ x} :=
 compl_singleton_eq x ▸ is_open_compl_iff.2 (t1_space.t1 x)
 
+instance subtype.t1_space {α : Type u} [topological_space α] [t1_space α] {p : α → Prop} :
+  t1_space (subtype p) :=
+⟨λ ⟨x, hx⟩, is_closed_induced_iff.2 $ ⟨{x}, is_closed_singleton, set.ext $ λ y,
+  by simp [subtype.coe_ext]⟩⟩
+
 @[priority 100] -- see Note [lower instance priority]
 instance t1_space.t0_space [t1_space α] : t0_space α :=
 ⟨λ x y h, ⟨{z | z ≠ y}, is_open_ne, or.inl ⟨h, not_not_intro rfl⟩⟩⟩
@@ -320,6 +270,15 @@ let ⟨t, ht₁, ht₂, ht₃⟩ := this in
   subset.trans (compl_subset_comm.1 ht₂) h₁,
   is_closed_compl_iff.mpr ht₁⟩
 
+instance subtype.regular_space [regular_space α] {p : α → Prop} : regular_space (subtype p) :=
+⟨begin
+   intros s a hs ha,
+   rcases is_closed_induced_iff.1 hs with ⟨s, hs', rfl⟩,
+   rcases regular_space.regular hs' ha with ⟨t, ht, hst, hat⟩,
+   refine ⟨coe ⁻¹' t, is_open_induced ht, preimage_mono hst, _⟩,
+   rw [nhds_induced, ← comap_principal, ← comap_inf, hat, comap_bot]
+ end⟩
+
 variable (α)
 @[priority 100] -- see Note [lower instance priority]
 instance regular_space.t2_space [regular_space α] : t2_space α :=