compls — Mathlib

English

Analogous sized-complements statement for sets: Set.Sized n 𝒜ᶜˢ.toSet ↔ Set.Sized (|α| − n) 𝒜.toSet under finiteness assumptions.

Русский

Аналогично для множеств: Set.Sized n 𝒜ᶜˢ.toSet ⇔ Set.Sized (|α| − n) 𝒜.toSet при условиях конечности.

LaTeX

$$$\text{Set.Sized } n 𝒜^{\!c_s.toSet} \iff \text{Set.Sized } (|α| - n) 𝒜.toSet$$$

Lean4

protected theorem _root_.Set.Sized.compls (h𝒜 : (𝒜 : Set (Finset α)).Sized n) :
    (𝒜ᶜˢ : Set (Finset α)).Sized (Fintype.card α - n) :=
  Finset.forall_mem_compls.2 <| fun s hs ↦ by rw [Finset.card_compl, h𝒜 hs]

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