feat(topology/subset_properties): an infinite type with cofinite topology is irreducible (#16499)

Author: urkud

src/data/set/basic.lean

@@ -1914,6 +1914,9 @@ by simp_rw [set.subsingleton, set.nontrivial, not_forall]
 @[simp] lemma not_nontrivial_iff : ¬ s.nontrivial ↔ s.subsingleton :=
 iff.not_left not_subsingleton_iff.symm
 
+alias not_nontrivial_iff ↔ _ subsingleton.not_nontrivial
+alias not_subsingleton_iff ↔ _ nontrivial.not_subsingleton
+
 theorem univ_eq_true_false : univ = ({true, false} : set Prop) :=
 eq.symm $ eq_univ_of_forall $ classical.cases (by simp) (by simp)
 

src/topology/separation.lean

@@ -1269,7 +1269,7 @@ begin
     compact_closure_of_subset_compact hV interior_subset⟩,
 end
 
-lemma is_preirreducible_iff_subsingleton [t2_space α] (S : set α) :
+lemma is_preirreducible_iff_subsingleton [t2_space α] {S : set α} :
   is_preirreducible S ↔ S.subsingleton :=
 begin
   refine ⟨λ h x hx y hy, _, set.subsingleton.is_preirreducible⟩,
@@ -1278,11 +1278,19 @@ begin
   exact ((h U V hU hV ⟨x, hx, hxU⟩ ⟨y, hy, hyV⟩).mono $ inter_subset_right _ _).not_disjoint h',
 end
 
-lemma is_irreducible_iff_singleton [t2_space α] (S : set α) :
+alias is_preirreducible_iff_subsingleton ↔ is_preirreducible.subsingleton _
+attribute [protected] is_preirreducible.subsingleton
+
+lemma is_irreducible_iff_singleton [t2_space α] {S : set α} :
   is_irreducible S ↔ ∃ x, S = {x} :=
 by rw [is_irreducible, is_preirreducible_iff_subsingleton,
   exists_eq_singleton_iff_nonempty_subsingleton]
 
+/-- There does not exist a nontrivial preirreducible T₂ space. -/
+lemma not_preirreducible_nontrivial_t2 (α) [topological_space α] [preirreducible_space α]
+  [nontrivial α] [t2_space α] : false :=
+(preirreducible_space.is_preirreducible_univ α).subsingleton.not_nontrivial nontrivial_univ
+
 end separation
 
 section regular_space

src/topology/sober.lean

@@ -223,7 +223,7 @@ instance t2_space.quasi_sober [t2_space α] : quasi_sober α :=
 begin
   constructor,
   rintro S h -,
-  obtain ⟨x, rfl⟩ := (is_irreducible_iff_singleton S).mp h,
+  obtain ⟨x, rfl⟩ := is_irreducible_iff_singleton.mp h,
   exact ⟨x, closure_singleton⟩
 end
 

src/topology/subset_properties.lean

@@ -1590,6 +1590,11 @@ theorem nonempty_preirreducible_inter [preirreducible_space α] {s t : set α} :
 by simpa only [univ_inter, univ_subset_iff] using
   @preirreducible_space.is_preirreducible_univ α _ _ s t
 
+/-- In a (pre)irreducible space, a nonempty open set is dense. -/
+protected theorem is_open.dense [preirreducible_space α] {s : set α} (ho : is_open s)
+  (hne : s.nonempty) : dense s :=
+dense_iff_inter_open.2 $ λ t hto htne, nonempty_preirreducible_inter hto ho htne hne
+
 theorem is_preirreducible.image {s : set α} (H : is_preirreducible s)
   (f : α → β) (hf : continuous_on f s) : is_preirreducible (f '' s) :=
 begin
@@ -1611,7 +1616,7 @@ end
 
 theorem is_irreducible.image {s : set α} (H : is_irreducible s)
   (f : α → β) (hf : continuous_on f s) : is_irreducible (f '' s) :=
-⟨nonempty_image_iff.mpr H.nonempty, H.is_preirreducible.image f hf⟩
+⟨H.nonempty.image _, H.is_preirreducible.image f hf⟩
 
 lemma subtype.preirreducible_space {s : set α} (h : is_preirreducible s) :
   preirreducible_space s :=
@@ -1633,6 +1638,17 @@ lemma subtype.irreducible_space {s : set α} (h : is_irreducible s) :
   (subtype.preirreducible_space h.is_preirreducible).is_preirreducible_univ,
   to_nonempty := h.nonempty.to_subtype }
 
+/-- An infinite type with cofinite topology is an irreducible topological space. -/
+@[priority 100] instance {α} [infinite α] : irreducible_space (cofinite_topology α) :=
+{ is_preirreducible_univ := λ u v,
+    begin
+      haveI : infinite (cofinite_topology α) := ‹_›,
+      simp only [cofinite_topology.is_open_iff, univ_inter],
+      intros hu hv hu' hv',
+      simpa only [compl_union, compl_compl] using ((hu hu').union (hv hv')).infinite_compl.nonempty
+    end,
+  to_nonempty := (infer_instance : nonempty α) }
+
 /-- A set `s` is irreducible if and only if
 for every finite collection of open sets all of whose members intersect `s`,
 `s` also intersects the intersection of the entire collection