biUnion_slice — Mathlib

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⟩⟩

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