eq_or_isStrictRestriction

Mathlib.Combinatorics.Matroid.Minor.Restrict

URI: https://scilib.ai/kg/mathlib#Matroid.IsRestriction.eq_or_isStrictRestriction

English

For every N ≤r M, either N = M or N <r M.

Русский

Для любого N ≤r M верно: либо N = M, либо N <r M.

LaTeX

$$$ N = M \lor N <_r M $$$

Lean4

theorem eq_or_isStrictRestriction (h : N ≤r M) : N = M ∨ N <r M := by simpa using eq_or_lt_of_le (ofMatroid_le_iff.2 h)

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

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

Разделы

Аффилиация

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