English
In the indiscrete topology, the only open sets are the empty set and the whole space.
Русский
В indiscrete топологии единственными открытыми множествами являются пустое множество и всё пространство.
LaTeX
$$$\\IsOpen[\\top] U \\iff (U = \\emptyset) \\lor (U = \\mathrm{univ})$$$
Lean4
/-- The only open sets in the indiscrete topology are the empty set and the whole space. -/
theorem isOpen_top_iff {α} (U : Set α) : IsOpen[⊤] U ↔ U = ∅ ∨ U = univ :=
⟨fun h => by
induction h with
| basic _ h => exact False.elim h
| univ => exact .inr rfl
| inter _ _ _ _ h₁ h₂ => rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
| sUnion _ _ ih => exact sUnion_mem_empty_univ ih,
by
rintro (rfl | rfl)
exacts [@isOpen_empty _ ⊤, @isOpen_univ _ ⊤]⟩
