dual_rankPos

Mathlib.Combinatorics.Matroid.Circuit

URI: https://scilib.ai/kg/mathlib#Matroid.IsCircuit.dual_rankPos

English

If M is circuit on C, then the dual has RankPos.

Русский

Если C образует контур в M, то двойственный матроид имеет RankPos.

LaTeX

$$$\text{IsCircuit}_M(C) \Rightarrow M^{\ast}.RankPos$$$

Lean4

theorem dual_rankPos (hC : M.IsCircuit C) : M✶.RankPos :=
  dual_rankPos_iff_exists_isCircuit.mpr ⟨C, hC⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru