indep_delete_of_disjoint

Mathlib.Combinatorics.Matroid.Minor.Delete

URI: https://scilib.ai/kg/mathlib#Matroid.Indep.indep_delete_of_disjoint

English

If M.Indep I and Disjoint I D, then (M \\ D).Indep I.

Русский

Если I независим в M и Disjoint(I,D), то (M \\ D).Indep I.

LaTeX

$$$M.Indep I \\land \\operatorname{Disjoint}(I,D) \\rightarrow (M\\setminus D).Indep I$$$

Lean4

theorem indep_delete_of_disjoint (h : M.Indep I) (hID : Disjoint I D) : (M ＼ D).Indep I :=
  delete_indep_iff.mpr ⟨h, hID⟩

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

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

Разделы

Аффилиация

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