delete_rankPos

Mathlib.Combinatorics.Matroid.Minor.Delete

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

English

RankPos is preserved under deletion when M has RankPos.

Русский

RankPos сохраняется после удаления D, если исходно M имеет RankPos.

LaTeX

$$$ [M.RankPos] \Rightarrow (M \setminus D).RankPos $$$

Lean4

theorem delete_rankPos [M.RankPos] (hD : M.Coindep D) : (M ＼ D).RankPos :=
  by
  rw [rankPos_iff, hD.delete_isBase_iff]
  simp [M.empty_not_isBase]

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

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

Разделы

Аффилиация

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