trans_isStrictMinor

Mathlib.Combinatorics.Matroid.Minor.Order

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

English

If N is a minor of M and M is a strict minor of M', then N is a strict minor of M'.

Русский

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

LaTeX

$$N ≤m M → M

Lean4

theorem trans_isStrictMinor (h : N ≤m M) (h' : M <m M') : N <m M' :=
  h.le.trans_lt h'

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

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

Разделы

Аффилиация

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