feat(topology/subset_properties): add instances for totally_disconnec…

…ted_spaces (#5334)

Add the instances subtype.totally_disconnected_space and pi.totally_disconnected_space.

src/data/set/basic.lean

@@ -1470,6 +1470,12 @@ begin
   { exact λ h, subsingleton.intro (λ a b, set_coe.ext (h a.property b.property)) }
 end
 
+/-- `s` is a subsingleton, if its image of an injective function is. -/
+theorem subsingleton_of_image {α β : Type*} {f : α → β} (hf : function.injective f)
+  (s : set α) (hs : subsingleton (f '' s)) : subsingleton s :=
+subsingleton.intro $ λ ⟨a, ha⟩ ⟨b, hb⟩, subtype.ext $ hf
+  (by {simpa using @subsingleton.elim _ hs ⟨f a, ⟨a, ha, rfl⟩⟩ ⟨f b, ⟨b, hb, rfl⟩⟩})
+
 theorem univ_eq_true_false : univ = ({true, false} : set Prop) :=
 eq.symm $ eq_univ_of_forall $ classical.cases (by simp) (by simp)
 

src/topology/subset_properties.lean

@@ -1263,6 +1263,25 @@ from (eq_of_mem_singleton (ht hp)).symm ▸ (eq_of_mem_singleton (ht hq)).symm
 class totally_disconnected_space (α : Type u) [topological_space α] : Prop :=
 (is_totally_disconnected_univ : is_totally_disconnected (univ : set α))
 
+instance pi.totally_disconnected_space {α : Type*} {β : α → Type*} [t₂ : Πa, topological_space (β a)]
+  [∀a, totally_disconnected_space (β a)] : totally_disconnected_space (Π (a : α), β a) :=
+⟨λ t h1 h2, ⟨λ a b, subtype.ext $ funext $ λ x, subtype.mk_eq_mk.1 $
+  (totally_disconnected_space.is_totally_disconnected_univ
+    ((λ (c : Π (a : α), β a), c x) '' t) (set.subset_univ _)
+    (is_preconnected.image h2 _ (continuous.continuous_on (continuous_apply _)))).cases_on
+  (λ h3, h3
+    ⟨(a.1 x), by {simp only [set.mem_image, subtype.val_eq_coe], use a, split,
+      simp only [subtype.coe_prop]}⟩
+    ⟨(b.1 x), by {simp only [set.mem_image, subtype.val_eq_coe], use b, split,
+      simp only [subtype.coe_prop]}⟩)⟩⟩
+
+instance subtype.totally_disconnected_space {α : Type*} {p : α → Prop} [topological_space α]
+  [totally_disconnected_space α] : totally_disconnected_space (subtype p) :=
+⟨λ s h1 h2,
+  set.subsingleton_of_image subtype.val_injective s (
+    totally_disconnected_space.is_totally_disconnected_univ (subtype.val '' s) (set.subset_univ _)
+      ((is_preconnected.image h2 _) (continuous.continuous_on (@continuous_subtype_val _ _ p))))⟩
+
 end totally_disconnected
 
 section totally_separated