contract_delete_isMinor

Mathlib.Combinatorics.Matroid.Minor.Order

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

English

The minor obtained by contracting C and deleting D is a minor of M.

Русский

Минор, полученный после сокращения C и удаления D, является минором M.

LaTeX

$$$ M/\!C \setminus D \le_m M $$$

Lean4

@[simp]
theorem contract_delete_isMinor (M : Matroid α) (C D : Set α) : M ／ C ＼ D ≤m M :=
  ⟨C, D, rfl⟩

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

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

Разделы

Аффилиация

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