deleteElem_eq_self

Mathlib.Combinatorics.Matroid.Minor.Delete

URI: https://scilib.ai/kg/mathlib#Matroid.deleteElem_eq_self

English

If an element e is not in the ground E(M), then deleting {e} from M has no effect: M \\ {e} = M.

Русский

Если элемент e не принадлежит основанию E(M), то удаление {e} не меняет матроид: M \\ {e} = M.

LaTeX

$$$e\\notin M.E \\Rightarrow M\\setminus\\{e\\} = M$$$

Lean4

theorem deleteElem_eq_self (he : e ∉ M.E) : M ＼ { e } = M := by simpa

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

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

Разделы

Аффилиация

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