IsStrictMinor

Mathlib.Combinatorics.Matroid.Minor.Order

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

← MathLib Explorer

English

If N is a minor of M, then N.E ⊆ M.E.

Русский

Если N является минором M, то множества E(N) ⊆ E(M).

LaTeX

$$$ N \le_m M \Rightarrow N.E \subseteq M.E $$$

Lean4

/-- `N` is a strict minor of `M` if `N` is a minor of `M` and `N ≠ M`.
Equivalently, `N` is obtained from `M` by deleting/contracting subsets of the ground set
that are not both empty. -/
def IsStrictMinor (N M : Matroid α) : Prop :=
  N ≤m M ∧ ¬M ≤m N

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

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

Разделы

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

Аффилиация

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