English
A space is Alexandrov discrete iff unions of closed sets are closed: for every collection S of subsets, if every member of S is closed, then the union of S is closed.
Русский
Пространство Александрова-дискретно тогда и только тогда, когда объединение замкнутых множеств замкнуто: для каждой семейства S частью S каждый элемент замкнут, следовательно ⋃S замкнуто.
LaTeX
$$$\text{AlexandrovDiscrete}(\alpha) \iff \forall S:\text{Set}(\text{Set}(\alpha)),(\forall s\in S,\ IsClosed(s))\to IsClosed(⋃_{s\in S} s)$$$
Lean4
theorem alexandrovDiscrete_iff_isClosed :
AlexandrovDiscrete α ↔ ∀ S : Set (Set α), (∀ s ∈ S, IsClosed s) → IsClosed (⋃₀ S) := by
conv_lhs =>
tactic =>
simp_rw +singlePass [alexandrovDiscrete_iff, compl_surjective.image_surjective.forall, forall_mem_image, ←
compl_sUnion, isOpen_compl_iff]
