English
The sum of two matroids M on α and N on β is a matroid on the disjoint sum α ⊕ β, constructed by combining their structure via a sigma-construction and a pairing of the two ground sets.
Русский
Сумма двух матроидов M на α и N на β образует матроид на дизьjoint-sum α ⊕ β, которая строится объединением структур через σ-конструкцию и сопоставлением двух оснований.
LaTeX
$$$$ (M.sum N) : \text{Matroid}(\alpha \oplus \beta). $$$$
Lean4
/-- The sum of two matroids as a matroid on the sum type. -/
protected def sum (M : Matroid α) (N : Matroid β) : Matroid (α ⊕ β) :=
let S := Matroid.sigma (Bool.rec (M.mapEquiv Equiv.ulift.symm) (N.mapEquiv Equiv.ulift.symm))
let e := Equiv.sumEquivSigmaBool (ULift.{v} α) (ULift.{u} β)
(S.mapEquiv e.symm).mapEquiv (Equiv.sumCongr Equiv.ulift Equiv.ulift)
