contract_eq_loopyOn — Mathlib

English

Let M be a matroid on a ground set, and let X be a subset that spans M. Then the contraction of M by X is exactly the loopy matroid on the complement of X within the ground set: M / X = loopyOn(E \ X).

Русский

Пусть M — матроид над некоторым основанием, и X подмножество, спаннинг в M. Тогда сжатие M по X равняется матроид с петельками на дополнении X: M / X = loopyOn(E \ X).

LaTeX

$$$M / X = \mathrm{loopyOn}(M.E \setminus X)$$$

Lean4

theorem contract_eq_loopyOn (hX : M.Spanning X) : M ／ X = loopyOn (M.E \ X) :=
  by
  rw [eq_loopyOn_iff_loops_eq]
  simp [hX.closure_eq]

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