English
For a finite index set s and a family t of finite sets, the sigma-construction over t is equal to the union over i in s of the image of t(i) under the embedding sigmaMk i. In other words, there is a canonical decomposition of the sigma into the embedded parts.
Русский
Для конечного множества индексов s и семейства t из конечных множеств выполняется, что сигма-конструкция над t равна объединению по i в s образов t(i) под вложением sigmaMk i. То есть существует каноническое разложение сигмы на встроенные части.
LaTeX
$$$$ s.\sigma t = s.\biUnion\; (i \mapsto (t(i)).map \bigl(\mathrm{Embedding.sigmaMk}\, i\bigr)) $$$$
Lean4
theorem sigma_eq_biUnion [DecidableEq (Σ i, α i)] (s : Finset ι) (t : ∀ i, Finset (α i)) :
s.sigma t = s.biUnion fun i => (t i).map <| Embedding.sigmaMk i :=
by
ext ⟨x, y⟩
simp [and_left_comm]
