case mp
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ TotallyDisconnectedSpace α → ∀ (x : α), Set.Subsingleton (connectedComponent x)

case mpr
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∀ (x : α), Set.Subsingleton (connectedComponent x)) → TotallyDisconnectedSpace α
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), Set.Subsingleton (connectedComponent x)
constructor
case mpr
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), Set.Subsingleton (connectedComponent x)
⊢ TotallyDisconnectedSpace α
case mpr
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∀ (x : α), Set.Subsingleton (connectedComponent x)) → TotallyDisconnectedSpace α
intro h
case mpr.isTotallyDisconnected_univ
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), Set.Subsingleton (connectedComponent x)
⊢ IsTotallyDisconnected univ
case mpr
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), Set.Subsingleton (connectedComponent x)
⊢ TotallyDisconnectedSpace α
constructor
case mpr.isTotallyDisconnected_univ
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s✝ t u v : Set α
h : ∀ (x : α), Set.Subsingleton (connectedComponent x)
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
⊢ Set.Subsingleton s
case mpr.isTotallyDisconnected_univ
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), Set.Subsingleton (connectedComponent x)
⊢ IsTotallyDisconnected univ
intro s s_sub hs
case mpr.isTotallyDisconnected_univ.inl
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), Set.Subsingleton (connectedComponent x)
s_sub : ∅ ⊆ univ
hs : IsPreconnected ∅
⊢ Set.Subsingleton ∅

case mpr.isTotallyDisconnected_univ.inr.intro
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s✝ t u v : Set α
h : ∀ (x : α), Set.Subsingleton (connectedComponent x)
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
x : α
x_in : x ∈ s
⊢ Set.Subsingleton s
case mpr.isTotallyDisconnected_univ
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s✝ t u v : Set α
h : ∀ (x : α), Set.Subsingleton (connectedComponent x)
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
⊢ Set.Subsingleton s
rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩)
case mp
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : TotallyDisconnectedSpace α
x : α
⊢ Set.Subsingleton (connectedComponent x)
case mp
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ TotallyDisconnectedSpace α → ∀ (x : α), Set.Subsingleton (connectedComponent x)
intro h x
case mp.a
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : TotallyDisconnectedSpace α
x : α
⊢ connectedComponent x ⊆ univ

case mp.a
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : TotallyDisconnectedSpace α
x : α
⊢ IsPreconnected (connectedComponent x)
case mp
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : TotallyDisconnectedSpace α
x : α
⊢ Set.Subsingleton (connectedComponent x)
apply h.1
no goals
case mp.a
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : TotallyDisconnectedSpace α
x : α
⊢ IsPreconnected (connectedComponent x)
exact isPreconnected_connectedComponent
no goals
case mp.a
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : TotallyDisconnectedSpace α
x : α
⊢ connectedComponent x ⊆ univ
exact subset_univ _
no goals
case mpr.isTotallyDisconnected_univ.inl
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), Set.Subsingleton (connectedComponent x)
s_sub : ∅ ⊆ univ
hs : IsPreconnected ∅
⊢ Set.Subsingleton ∅
exact subsingleton_empty
no goals
case mpr.isTotallyDisconnected_univ.inr.intro
α : Type u
β : Type v
ι : Type ?u.122534
π : ι → Type ?u.122539
inst✝ : TopologicalSpace α
s✝ t u v : Set α
h : ∀ (x : α), Set.Subsingleton (connectedComponent x)
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
x : α
x_in : x ∈ s
⊢ Set.Subsingleton s
exact (h x).anti (hs.subset_connectedComponent x_in)