closure_compl

Mathlib.Combinatorics.Matroid.Closure

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

English

If I is coindependent, then closure of the complement of the ground is the ground.

Русский

Если I коиндепендентно, то замыкание дополнения множества E равно E.

LaTeX

$$$$ M.Coindep I \Rightarrow M.closure (M.E \setminus I) = M.E. $$$$

Lean4

theorem closure_compl (hX : M.Coindep X) : M.closure (M.E \ X) = M.E :=
  (coindep_iff_closure_compl_eq_ground hX.subset_ground).mp hX

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

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

Разделы

Аффилиация

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