stableUnderSpecialization_compl_iff

English

For every subset s of a topological space X, the complement s^c is stable under specialization if and only if s is stable under generalization.

Русский

Для произвольного подмножества s пространства X, дополнение s^c стабильно по специализации тогда и только тогда, когда s стабильно по обобщению.

LaTeX

$$$StableUnderSpecialization(s^c) \iff StableUnderGeneralization(s)$$$

Lean4

@[simp]
theorem stableUnderSpecialization_compl_iff {s : Set X} : StableUnderSpecialization sᶜ ↔ StableUnderGeneralization s :=
  isLowerSet_compl

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