English
The disjointSigma construction builds a matroid on α from a family of matroids with pairwise disjoint ground sets by taking a sigma-construction after restricting each piece to its ground set and embedding via a sumSet-like map.
Русский
Конструкция disjointSigma строит матроид на α из семейства матроидов с попарно непересекающимися множествами оснований, применяя σ-конструкцию после ограничения каждого компонента до его основания и вложения через некое отображение суммирования.
LaTeX
$$$$ \text{DisjointSigma}(M,h) : \text{Matroid}(\alpha). $$$$
Lean4
/-- The sum of an indexed collection of matroids on `α` with pairwise disjoint ground sets,
as a matroid on `α` -/
protected def disjointSigma (M : ι → Matroid α) (h : Pairwise (Disjoint on fun i ↦ (M i).E)) : Matroid α :=
(Matroid.sigma (fun i ↦ (M i).restrictSubtype (M i).E)).mapEmbedding (Function.Embedding.sigmaSet h)
