contract_indep_diff_iff — Mathlib

English

Let M be a matroid on a set α and assume I is a basis of X in M (I is a basis for X inside M). Then for any sets J and X, the subset J \\ X is independent in the contracted matroid M / X if and only if the union (J \\ X) ∪ I is independent in M.

Русский

Пусть M — матроид на множествах α, и пусть I является базисом X в M. Тогда для любых множеств J и X подмножество J \ X независимо в сокращенном матроиде M / X тогда и только тогда, когда объединение (J \ X) ∪ I независимо в M.

LaTeX

$$$(M / X).Indep(J \\ X) \\iff M.Indep((J \\ X) \\cup I)$$$

Lean4

theorem contract_indep_diff_iff (hI : M.IsBasis' I X) : (M ／ X).Indep (J \ X) ↔ M.Indep ((J \ X) ∪ I) := by
  rw [hI.contract_indep_iff, and_iff_left disjoint_sdiff_right]

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