upShadow — Mathlib

English

The upper shadow of r-sets is a family of (r+1)-sets.

Русский

Верхняя тень наборов размера r является семейством наборов размера r+1.

LaTeX

$$$ Set.Sized.upShadow( h𝒜 ) \;:\; (𝒜 : Set( Finset(α) )).Sized r \Rightarrow (∂⁺ 𝒜 : Set( Finset(α) )).Sized (r+1) $$$

Lean4

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

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