of_delete

Mathlib.Combinatorics.Matroid.Minor.Delete

URI: https://scilib.ai/kg/mathlib#Matroid.IsBasis.of_delete

English

If a subset I is a basis of X in the minor M \ D, then I is a basis of X in M.

Русский

Пусть I является базисом X в производном от M, полученном удалением D; тогда I является базисом X в M.

LaTeX

$$$ (M \setminus D).IsBasis(I,X) \Rightarrow M.IsBasis(I,X) $$$

Lean4

theorem of_delete (h : (M ＼ D).IsBasis I X) : M.IsBasis I X :=
  (delete_isBasis_iff.mp h).1

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

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

Разделы

Аффилиация

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