mem_of_isBase

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsColoop.mem_of_isBase

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_isBase (he : M.IsColoop e) (hB : M.IsBase B) : e ∈ B :=
  isColoop_iff_forall_mem_isBase.mp he hB

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

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

Разделы

Аффилиация

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