exists_isBase_subset_compl

Mathlib.Combinatorics.Matroid.Dual

URI: https://scilib.ai/kg/mathlib#Matroid.Coindep.exists_isBase_subset_compl

English

If X is coindependent in M, there exists a base B with B ⊆ E \ X.

Русский

Если X коиндепендентно в M, существует база B такая, что B ⊆ E \ X.

LaTeX

$$(coindep_iff_exists h.subset_ground).1 h$$

Lean4

theorem exists_isBase_subset_compl (h : M.Coindep X) : ∃ B, M.IsBase B ∧ B ⊆ M.E \ X :=
  (coindep_iff_exists h.subset_ground).1 h

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

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

Разделы

Аффилиация

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