English
For every k, the union of the k-th slice 𝒜 #k with the shadow of the (k+1)-st falling equals the k-th falling 𝒜: 𝒜 #k ∪ ∂ (falling (k+1) 𝒜) = falling k 𝒜.
Русский
Для каждого k объединение к-го слоя 𝒜 и тени (k+1)-й падения 𝒜 равно k-му падению 𝒜: 𝒜 #k ∪ ∂ (falling (k+1) 𝒜) = falling k 𝒜.
LaTeX
$$$$ 𝒜 \\#k \\cup \\partial (falling (k+1) 𝒜) = falling k 𝒜 $$$$
Lean4
theorem slice_union_shadow_falling_succ : 𝒜 #k ∪ ∂ (falling (k + 1) 𝒜) = falling k 𝒜 :=
by
ext s
simp_rw [mem_union, mem_slice, mem_shadow_iff, mem_falling]
constructor
· rintro (h | ⟨s, ⟨⟨t, ht, hst⟩, hs⟩, a, ha, rfl⟩)
· exact ⟨⟨s, h.1, Subset.refl _⟩, h.2⟩
refine ⟨⟨t, ht, (erase_subset _ _).trans hst⟩, ?_⟩
rw [card_erase_of_mem ha, hs]
rfl
· rintro ⟨⟨t, ht, hst⟩, hs⟩
by_cases h : s ∈ 𝒜
· exact Or.inl ⟨h, hs⟩
obtain ⟨a, ha, hst⟩ := ssubset_iff.1 (ssubset_of_subset_of_ne hst (ht.ne_of_notMem h).symm)
refine Or.inr ⟨insert a s, ⟨⟨t, ht, hst⟩, ?_⟩, a, mem_insert_self _ _, erase_insert ha⟩
rw [card_insert_of_notMem ha, hs]
