shadow — Mathlib

English

The shadow of a family of r-sets is a family of r−1-sets.

Русский

Тень семейства r-множеств — это семейство множеств размера r−1.

LaTeX

$$$$ \\partial 𝒜 : \\text{Sized}(r-1) $$$$

Lean4

/-- The shadow of a family of `r`-sets is a family of `r - 1`-sets. -/
protected theorem _root_.Set.Sized.shadow (h𝒜 : (𝒜 : Set (Finset α)).Sized r) : (∂ 𝒜 : Set (Finset α)).Sized (r - 1) :=
  by
  intro A h
  obtain ⟨A, hA, i, hi, rfl⟩ := mem_shadow_iff.1 h
  rw [card_erase_of_mem hi, h𝒜 hA]

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