no goals
α : Type u
β : Type v
ι : Type ?u.69730
π : ι → Type ?u.69735
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : PreconnectedSpace α
s : Set α
hs : IsClopen s
h : ¬(s = ∅ ∨ s = univ)
h2 : sᶜ = ∅
⊢ s = univ
rw [← compl_compl s, h2, compl_empty]
no goals
α : Type u
β : Type v
ι : Type ?u.69730
π : ι → Type ?u.69735
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : PreconnectedSpace α
s : Set α
⊢ s = ∅ ∨ s = univ → IsClopen s
rintro (rfl | rfl) <;> [exact isClopen_empty; exact isClopen_univ]