coloops_indep — Mathlib

English

If two matroids M1 and M2 have the same ground E, the same loops and coloops, and agree on independent sets after removing loops/coloops, then M1 = M2.

Русский

Если два матроида M1 и M2 имеют одну и ту же базовую множество E, одинаковые циклы и колоопы, и их независимые множества после удаления петель и колоопов совпадают, то M1 = M2.

LaTeX

$$$$ M_1.E = M_2.E \;\land\; M_1.loops = M_2.loops \;\land\; M_1.coloops = M_2.coloops \land \forall I \subseteq M_1.E, (M_1.Indep(I) \iff M_2.Indep(I)) \Rightarrow M_1 = M_2. $$$$

Lean4

theorem coloops_indep (M : Matroid α) : M.Indep M.coloops :=
  by
  rw [← empty_union M.coloops, union_coloops_indep_iff]
  exact M.empty_indep

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