exists_isCircuit

Mathlib.Combinatorics.Matroid.Circuit

URI: https://scilib.ai/kg/mathlib#Matroid.exists_isCircuit

English

If RankPos holds for the dual, there exists a circuit in M.

Русский

Если существует RankPos двойственного, то в M существует контур.

LaTeX

$$[RankPos M✶] ⟹ ∃ C, M.IsCircuit(C)$$

Lean4

theorem exists_isCircuit [RankPos M✶] : ∃ C, M.IsCircuit C :=
  dual_rankPos_iff_exists_isCircuit.1 (by assumption)

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

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

Разделы

Аффилиация

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