English
In a preconnected space, a set is clopen if and only if it is either empty or the whole space.
Русский
В предсвязанном пространстве множество является одновременно открытым и закрытым тогда и только тогда, когда оно пустое или всё пространство.
LaTeX
$$$\text{IsClopen}(s) \iff (s = \emptyset) \lor (s = \text{univ})$$$
Lean4
theorem isClopen_iff [PreconnectedSpace α] {s : Set α} : IsClopen s ↔ s = ∅ ∨ s = univ :=
⟨fun hs =>
by_contradiction fun h =>
have h1 : s ≠ ∅ ∧ sᶜ ≠ ∅ :=
⟨mt Or.inl h, mt (fun h2 => Or.inr <| (by rw [← compl_compl s, h2, compl_empty] : s = univ)) h⟩
let ⟨_, h2, h3⟩ :=
nonempty_inter hs.2 hs.1.isOpen_compl (union_compl_self s) (nonempty_iff_ne_empty.2 h1.1)
(nonempty_iff_ne_empty.2 h1.2)
h3 h2,
by rintro (rfl | rfl) <;> [exact isClopen_empty; exact isClopen_univ]⟩
