Theorem: IsCountable.isTotallyDisconnected (Ray/Misc/TotallyDisconnected.lean)

State before:
X : Type
inst✝ : MetricSpace X
s : Set X
h : s.Countable
⊢ IsTotallyDisconnected s
Tactic:
rw [← isTotallyDisconnected_iff_totally_disconnected_subtype]
State after:
X : Type
inst✝ : MetricSpace X
s : Set X
h : s.Countable
⊢ TotallyDisconnectedSpace ↑s

State before:
X : Type
inst✝ : MetricSpace X
s : Set X
h : s.Countable
⊢ TotallyDisconnectedSpace ↑s
Tactic:
exact @Countable.totallyDisconnectedSpace _ _ (countable_coe_iff.mpr h)
State after:
no goals