case mp
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ ConnectedSpace α → ∃ x, connectedComponent x = univ

case mpr
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∃ x, connectedComponent x = univ) → ConnectedSpace α
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ ConnectedSpace α ↔ ∃ x, connectedComponent x = univ
constructor
case mp.mk.intro
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
toPreconnectedSpace✝ : PreconnectedSpace α
x : α
⊢ ∃ x, connectedComponent x = univ
case mp
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ ConnectedSpace α → ∃ x, connectedComponent x = univ
rintro ⟨⟨x⟩⟩
no goals
case mp.mk.intro
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
toPreconnectedSpace✝ : PreconnectedSpace α
x : α
⊢ ∃ x, connectedComponent x = univ
exact
  ⟨x, eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)⟩
case mpr.intro
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
h : connectedComponent x = univ
⊢ ConnectedSpace α
case mpr
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∃ x, connectedComponent x = univ) → ConnectedSpace α
rintro ⟨x, h⟩
case mpr.intro
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
h : connectedComponent x = univ
this : PreconnectedSpace α
⊢ ConnectedSpace α
case mpr.intro
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
h : connectedComponent x = univ
⊢ ConnectedSpace α
haveI : PreconnectedSpace α :=
  ⟨by rw [← h]; exact isPreconnected_connectedComponent⟩
no goals
case mpr.intro
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
h : connectedComponent x = univ
this : PreconnectedSpace α
⊢ ConnectedSpace α
exact ⟨⟨x⟩⟩
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected (connectedComponent x)
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected univ
rw [← h]
no goals
α : Type u
β : Type v
ι : Type ?u.63292
π : ι → Type ?u.63297
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected (connectedComponent x)
exact isPreconnected_connectedComponent