stableUnderGeneralization_compl_iff

English

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

Русский

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

LaTeX

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

Lean4

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

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