α : Type u
β : Type v
ι : Type ?u.122829
π : ι → Type ?u.122834
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∀ (x : α), Set.Subsingleton (connectedComponent x)) ↔ ∀ (x : α), connectedComponent x = {x}
α : Type u
β : Type v
ι : Type ?u.122829
π : ι → Type ?u.122834
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}
rw [totallyDisconnectedSpace_iff_connectedComponent_subsingleton]
α : Type u
β : Type v
ι : Type ?u.122829
π : ι → Type ?u.122834
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
⊢ Set.Subsingleton (connectedComponent x) ↔ connectedComponent x = {x}
α : Type u
β : Type v
ι : Type ?u.122829
π : ι → Type ?u.122834
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∀ (x : α), Set.Subsingleton (connectedComponent x)) ↔ ∀ (x : α), connectedComponent x = {x}
refine forall_congr' fun x => ?_
α : Type u
β : Type v
ι : Type ?u.122829
π : ι → Type ?u.122834
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
⊢ x ∈ connectedComponent x
α : Type u
β : Type v
ι : Type ?u.122829
π : ι → Type ?u.122834
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
⊢ Set.Subsingleton (connectedComponent x) ↔ connectedComponent x = {x}
rw [subsingleton_iff_singleton]
no goals
α : Type u
β : Type v
ι : Type ?u.122829
π : ι → Type ?u.122834
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
⊢ x ∈ connectedComponent x
exact mem_connectedComponent