not_isMinor

Mathlib.Combinatorics.Matroid.Minor.Order

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

English

If N is a strict minor of M, then M is not a minor of N.

Русский

Если N является строгим минором M, то M не является минором N.

LaTeX

$$(N

Lean4

theorem not_isMinor (h : N <m M) : ¬(M ≤m N) :=
  h.lt.not_ge

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

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

Разделы

Аффилиация

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