English
Let s be a finite set of indices and t(i) be finite sets for each i in s. Then the disjoint union of the sets t(i), transported into the sigma-type via the canonical embedding, over all i in s, equals the sigma-construction of the family t. In particular, this gives a decomposition of the sigma-t into the embedded components, and the pieces are pairwise disjoint.
Русский
Пусть s — конечное подмножество индексов, для каждого i в s задано конечное множество t(i). Тогда попарно несоприкасаемое объединение вкладов t(i), переведённых в сигма-тип через каноническое вложение, по всем i в s равно сигма-конструкция над семейством t. В частности, сигма-разложение над t разлагается на вложенные компоненты, которые попарно не пересекаются.
LaTeX
$$$$ s\mathrm{.disjiUnion}\bigl(i \mapsto (t(i)).\mathrm{map}(\mathrm{Embedding.sigmaMk}\, i)\bigr)\;=\;s\mathrm{.sigma}\;t $$$$
Lean4
@[simp]
theorem disjiUnion_map_sigma_mk :
s.disjiUnion (fun i => (t i).map (Embedding.sigmaMk i)) pairwiseDisjoint_map_sigmaMk = s.sigma t :=
rfl
