English
The union of all r-slices over r up to card α recovers 𝒜.
Русский
Объединение всех r-срезов с 0 до |α| восстанавливает 𝒜.
LaTeX
$$$ (Iic\lvert \alpha\rvert).\biUnion 𝒜.\text{slice} = 𝒜 $$$
Lean4
@[simp]
theorem biUnion_slice [DecidableEq α] : (Iic <| Fintype.card α).biUnion 𝒜.slice = 𝒜 :=
Subset.antisymm (biUnion_subset.2 fun _r _ => slice_subset) fun s hs =>
mem_biUnion.2 ⟨#s, mem_Iic.2 <| s.card_le_univ, mem_slice.2 <| ⟨hs, rfl⟩⟩