delete_isBase_iff

Mathlib.Combinatorics.Matroid.Minor.Delete

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

English

The IsBase condition for M \\ D is equivalent to M being a Basis on B with ground M.E \\ D.

Русский

Условие IsBase для M \\ D эквивалентно тому, что M имеет базис B на множестве M.E \\ D.

LaTeX

$$$(M\\setminus D).IsBase B \\iff M.IsBasis B (M.E \\ D)$$

Lean4

@[simp]
theorem delete_isBase_iff : (M ＼ D).IsBase B ↔ M.IsBasis B (M.E \ D) := by rw [← restrict_compl, isBase_restrict_iff]

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

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

Разделы

Аффилиация

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