exists_subset_compl_isBase

Mathlib.Combinatorics.Matroid.Dual

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

English

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

Русский

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

LaTeX

$$coindep_iff_subset_compl_isBase.1 h$$

Lean4

theorem exists_subset_compl_isBase (h : M.Coindep X) : ∃ B, M.IsBase B ∧ X ⊆ M.E \ B :=
  coindep_iff_subset_compl_isBase.1 h

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

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

Разделы

Аффилиация

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