coloops_subset

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsBase.coloops_subset

English

All coloops lie in every base of the matroid.

Русский

Все колоопы содержатся в любом базисе матроидa.

LaTeX

$$(\\forall B)(M.IsBase B \\rightarrow M.coloops \\subseteq B)$$

Lean4

theorem coloops_subset (hB : M.IsBase B) : M.coloops ⊆ B := fun _ he ↦ IsColoop.mem_of_isBase he hB

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

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

Разделы

Аффилиация

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