English
A set s is stable under generalization if and only if there exists a family S of open sets whose intersection equals s.
Русский
Множество s стабильно по обобщению тогда и только тогда, когда существует семейство открытых множеств с пересечением, равным s.
LaTeX
$$$StableUnderGeneralization(s) \iff \exists S : Set(Set X), (\forall t \in S, IsOpen(t)) \land \bigcap_0 S = s$$
Lean4
/-- A set is stable under generalization iff it is an intersection of open sets. -/
theorem stableUnderGeneralization_iff_exists_sInter_eq {s : Set X} :
StableUnderGeneralization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s :=
by
refine ⟨?_, fun ⟨S, hS, e⟩ ↦ e ▸ stableUnderGeneralization_sInter S (fun x hx ↦ (hS x hx).stableUnderGeneralization)⟩
rw [← stableUnderSpecialization_compl_iff, stableUnderSpecialization_iff_exists_sUnion_eq]
exact fun ⟨S, h₁, h₂⟩ ↦
⟨(·ᶜ) '' S, fun s ⟨t, ht, e⟩ ↦ e ▸ (h₁ t ht).isOpen_compl,
compl_injective ((sUnion_eq_compl_sInter_compl S).symm.trans h₂)⟩
