eRk_eq

Mathlib.Combinatorics.Matroid.Rank.ENat

URI: https://scilib.ai/kg/mathlib#Matroid.IsLoop.eRk_eq

English

For a circuit C, eRk(C) + 1 = encard(C).

Русский

Для цикла C выполняется eRk(C) + 1 = encard(C).

LaTeX

$$If $M$ is a matroid and $C$ is a circuit, then $M.eRk(C) + 1 = C.encard$.$$

Lean4

theorem eRk_eq (he : M.IsLoop e) : M.eRk { e } = 0 := by
  rw [← eRk_closure_eq, he.closure, loops, eRk_closure_eq, eRk_empty]

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

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

Разделы

Аффилиация

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