IsMinor

Mathlib.Combinatorics.Matroid.Minor.Order

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

Lean4

/-- `N` is a minor of `M` if `N = M ／ C ＼ D` for some `C` and `D`.
The definition itself does not require `C` and `D` to be disjoint,
or even to be subsets of the ground set. See `Matroid.IsMinor.exists_eq_contract_delete_disjoint`
for the fact that we can choose `C` and `D` with these properties. -/
def IsMinor (N M : Matroid α) : Prop :=
  ∃ C D, N = M ／ C ＼ D

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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