English
Let I be a type indexing a family of matroids M i on the same ground set α. Then there is a natural matroid on the product ι × α, called the sum of the family, obtained by transporting the σ-construction along the natural equivalence between the σ-construction on M and the product indexing.
Русский
Пусть имеется индексированная семейство матроидов {M_i} над тем же основанием α. Существует естественная структура матроида на произведении ι × α, называемая суммой семейства, которая получается перенесением σ-конструкции через естественное эквиверенцию между σ-конструкцией для M и произведением индексов.
LaTeX
$$$$ (\operatorname{sum}' M) : \text{Matroid of } (\iota \times \alpha). $$$$
Lean4
/-- The sum of an indexed family `M : ι → Matroid α` of matroids on the same type,
as a matroid on the product type `ι × α`. -/
protected def sum' (M : ι → Matroid α) : Matroid (ι × α) :=
(Matroid.sigma M).mapEquiv <| Equiv.sigmaEquivProd ι α
