case mp
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ PreconnectedSpace α → ∀ (x : α), connectedComponent x = univ

case mpr
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∀ (x : α), connectedComponent x = univ) → PreconnectedSpace α
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ PreconnectedSpace α ↔ ∀ (x : α), connectedComponent x = univ
constructor
case mp
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : PreconnectedSpace α
x : α
⊢ connectedComponent x = univ
case mp
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ PreconnectedSpace α → ∀ (x : α), connectedComponent x = univ
intro h x
no goals
case mp
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : PreconnectedSpace α
x : α
⊢ connectedComponent x = univ
exact eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)
case mpr
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
⊢ PreconnectedSpace α
case mpr
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∀ (x : α), connectedComponent x = univ) → PreconnectedSpace α
intro h
case mpr.inl
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ PreconnectedSpace α

case mpr.inr
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ PreconnectedSpace α
case mpr
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
⊢ PreconnectedSpace α
cases' isEmpty_or_nonempty α with hα hα
no goals
case mpr.inl
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ PreconnectedSpace α
exact ⟨by rw [univ_eq_empty_iff.mpr hα]; exact isPreconnected_empty⟩
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected ∅
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected univ
rw [univ_eq_empty_iff.mpr hα]
no goals
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected ∅
exact isPreconnected_empty
no goals
case mpr.inr
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ PreconnectedSpace α
exact ⟨by rw [← h (Classical.choice hα)]; exact isPreconnected_connectedComponent⟩
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected (connectedComponent (Classical.choice hα))
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected univ
rw [← h (Classical.choice hα)]
no goals
α : Type u
β : Type v
ι : Type ?u.63690
π : ι → Type ?u.63695
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected (connectedComponent (Classical.choice hα))
exact isPreconnected_connectedComponent