English
Let 𝒜 be a family of finite subsets of α with ∅ not in 𝒜. Then the shadow ∂𝒜 consists of all sets obtained by removing one element from a member of 𝒜. Consequently, every set in ∂𝒜 has size r if and only if every set in 𝒜 has size r+1.
Русский
Пусть 𝒜 — семейство конечных подмножеств α, в котором пустое множество не принадлежит 𝒜. Теневое семейство ∂𝒜 состоит из всех множеств, получаемых вычеркиванием одного элемента из элемента 𝒜. Следовательно, все множества в ∂𝒜 имеют размер r тогда и только тогда, когда все множества в 𝒜 имеют размер r+1.
LaTeX
$$$ (\emptyset \notin 𝒜) \rightarrow \big( (\partial 𝒜 : Set(\Finset\ α)).Sized r \iff (𝒜 : Set(\Finset\ α)).Sized (r+1) \big) $$$
Lean4
theorem sized_shadow_iff (h : ∅ ∉ 𝒜) : (∂ 𝒜 : Set (Finset α)).Sized r ↔ (𝒜 : Set (Finset α)).Sized (r + 1) :=
by
refine ⟨fun h𝒜 s hs => ?_, Set.Sized.shadow⟩
obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 (ne_of_mem_of_not_mem hs h)
rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]
