English
The disjointSum of two matroids on α with ground sets disjoint is a matroid on α whose ground set is the union of the two grounds, formed by combining the two matroids via a sum-embedding.
Русский
Раздельная сумма двух матроидов на α с непересекающимися основаниями образует матроид на α, основанный на объединении оснований двух компонентов через отображение суммирования.
LaTeX
$$$$ (M disjointSum N h) : \text{Matroid}(\alpha). $$$$
Lean4
/-- The sum of two matroids on `α` with disjoint ground sets, as a `Matroid α`. -/
def disjointSum (M N : Matroid α) (h : Disjoint M.E N.E) : Matroid α :=
((M.restrictSubtype M.E).sum (N.restrictSubtype N.E)).mapEmbedding <| Function.Embedding.sumSet h
