sized_compls — Mathlib

English

Equivalent sized-complements statement for Finset level: for any 𝒜 : Finset (Finset α) and n ≤ card α, Set.Sized n 𝒜ᶜˢ.toSet ↔ Set.Sized (|α| − n) 𝒜.toSet.

Русский

Эквивалентно для конечного множества 𝒜: если n ≤ |α|, то Set.Sized n 𝒜ᶜˢ.toSet ⇔ Set.Sized (|α| − n) 𝒜.toSet.

LaTeX

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

Lean4

theorem sized_compls (hn : n ≤ Fintype.card α) :
    (𝒜ᶜˢ : Set (Finset α)).Sized n ↔ (𝒜 : Set (Finset α)).Sized (Fintype.card α - n)
    where
  mp h𝒜 := by simpa using h𝒜.compls
  mpr h𝒜 := by simpa only [Nat.sub_sub_self hn] using h𝒜.compls

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