isCobounded_ofBounded_iff — Mathlib

English

If B is a family of sets closed under required operations and includes all singletons, then s is cobounded iff s^c ∈ B.

Русский

Если B — семейство множеств, замкнутое по необходимым операциям и содержащее все одиночные множества, то s кобондировано тогда и только тогда, когда s^c ∈ B.

LaTeX

$$$\forall s,\text{IsCobounded}(s) \iff s^{\complement} \in B$$$

Lean4

theorem isCobounded_ofBounded_iff (B : Set (Set α)) {empty_mem subset_mem union_mem sUnion_univ} :
    @IsCobounded _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ) s ↔ sᶜ ∈ B :=
  Iff.rfl

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