mem_of_isColoop

Mathlib.Combinatorics.Matroid.Loop

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

English

If e is a coloop and B is a base, then e belongs to B.

Русский

Если e — колооп и B — базис, тогда e ∈ B.

LaTeX

$$$M.IsColoop e \\rightarrow (M.IsBase B \\rightarrow e \\in B)$$$

Lean4

theorem mem_of_isColoop (hB : M.IsBase B) (he : M.IsColoop e) : e ∈ B :=
  isColoop_iff_forall_mem_isBase.mp he hB

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

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

Разделы

Аффилиация

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