dual_isColoop

Mathlib.Combinatorics.Matroid.Loop

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

English

If e is a Loop in the dual matroid, then e is a Coloop in the original matroid; equivalently, dualizes the isLoop relation.

Русский

Если e является петлей в двойственном матроидe, то e является ColoOp в исходном.

LaTeX

$$M✶.IsLoop e \rightarrow M.IsColoop e$$

Lean4

theorem dual_isColoop (he : M.IsLoop e) : M✶.IsColoop e := by rwa [IsColoop, dual_dual]

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

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

Разделы

Аффилиация

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