stableUnderSpecialization_iff_Union_eq

English

A set s is stable under specialization if and only if the union over x in s of closures of {x} equals s.

Русский

Множество s устойчиво по специализации тогда и только тогда, когда объединение по x∈s замытий {x} равно s.

LaTeX

$$$StableUnderSpecialization(s) \iff \left(\bigcup_{x \in s} \overline{\{x\}}\right) = s$$$

Lean4

theorem stableUnderSpecialization_iff_Union_eq {s : Set X} :
    StableUnderSpecialization s ↔ (⋃ x ∈ s, closure { x }) = s :=
  Union_closure_singleton_eq_iff.symm

Похожие утверждения