coindep_contract_iff — Mathlib

English

For a matroid M and a subset C, a set X is coindependent in the contracted matroid M / C if and only if X is coindependent in M and X is disjoint from C.

Русский

Для матроида M и подмножества C множество X коиндепендентно в сокращённом матроидe M / C если и только если X коиндепендентно в M и X не пересекается с C.

LaTeX

$$$ (M / C).Coindep X \;\Leftrightarrow\; M.Coindep X \;\wedge\; \operatorname{Disjoint}(X, C) $$$

Lean4

theorem coindep_contract_iff : (M ／ C).Coindep X ↔ M.Coindep X ∧ Disjoint X C := by
  rw [coindep_def, dual_contract, delete_indep_iff, ← coindep_def]

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