compl_coindep

Mathlib.Combinatorics.Matroid.Closure

URI: https://scilib.ai/kg/mathlib#Matroid.Spanning.compl_coindep

English

If I is coindependent, then S = E is spanned by M.E \ I.

Русский

Если I коиндепендентно, то у M действительно есть множество, порождаемое E \ I.

LaTeX

$$$$ M.Spanning I \Rightarrow M.Coindep (M.E \ I). $$$$

Lean4

theorem compl_coindep (hS : M.Spanning S) : M.Coindep (M.E \ S) := by rwa [← spanning_iff_compl_coindep]

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

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

Разделы

Аффилиация

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