English
A set s is stable under specialization if and only if there exists a family S of closed sets whose union equals s.
Русский
Множество s устойчиво по специализации тогда и только тогда, когда существует семейство замкнутых множеств, чье объединение равно s.
LaTeX
$$$StableUnderSpecialization(s) \iff \exists S : Set(Set X), (\forall t \in S, IsClosed(t)) \land \bigcup_0 S = s$$
Lean4
/-- A set is stable under specialization iff it is a union of closed sets. -/
theorem stableUnderSpecialization_iff_exists_sUnion_eq {s : Set X} :
StableUnderSpecialization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = s :=
by
refine
⟨fun H ↦ ⟨(fun x : X ↦ closure { x }) '' s, ?_, ?_⟩, fun ⟨S, hS, e⟩ ↦
e ▸ stableUnderSpecialization_sUnion S (fun x hx ↦ (hS x hx).stableUnderSpecialization)⟩
· rintro _ ⟨_, _, rfl⟩; exact isClosed_closure
· conv_rhs => rw [← H.Union_eq]
simp
