sum_ground — Mathlib

English

The ground set of the sum of two matroids on disjoint domains is the union of the left- and right-injected ground sets.

Русский

Основание суммы двух матроидов на дизъюнктных основаниях равно объединению левой и правой инъекций оснований.

LaTeX

$$$$ (M.sum N).E = (\mathrm{inl}'' M.E) \cup (\mathrm{inr}'' N.E). $$$$

Lean4

@[simp]
theorem sum_ground (M : Matroid α) (N : Matroid β) : (M.sum N).E = (.inl '' M.E) ∪ (.inr '' N.E) := by
  simp [Matroid.sum, Set.ext_iff, mapEquiv, mapEmbedding, Equiv.ulift, Equiv.sumEquivSigmaBool]

Похожие утверждения