case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
H : Type u_1
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallyDisconnectedSpace H → TotallySeparatedSpace H

case mpr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
H : Type u_1
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallySeparatedSpace H → TotallyDisconnectedSpace H
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
H : Type u_1
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H
constructor
no goals
case mpr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
H : Type u_1
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallySeparatedSpace H → TotallyDisconnectedSpace H
apply TotallySeparatedSpace.totallyDisconnectedSpace
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
H : Type u_1
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
h : TotallyDisconnectedSpace H
⊢ TotallySeparatedSpace H
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
H : Type u_1
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
⊢ TotallyDisconnectedSpace H → TotallySeparatedSpace H
intro h
no goals
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
H : Type u_1
inst✝² : TopologicalSpace H
inst✝¹ : LocallyCompactSpace H
inst✝ : T2Space H
h : TotallyDisconnectedSpace H
⊢ TotallySeparatedSpace H
exact totallySeparatedSpace_of_t1_of_basis_clopen loc_compact_Haus_tot_disc_of_zero_dim