ofMatroid_lt_iff

Mathlib.Combinatorics.Matroid.Minor.Restrict

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

English

For matroids M, M': Matroidᵣ.ofMatroid M < Matroidᵣ.ofMatroid M' iff M <r M'.

Русский

Для матроидов M и M' выполняется: Matroidᵣ.ofMatroid M < Matroidᵣ.ofMatroid M' ⇔ M <r M'.

LaTeX

$$$ \\text{Matroid}ᵣ.ofMatroid\\ M < \\text{Matroid}ᵣ.ofMatroid\\ M' \\iff M <_r M' $$$

Lean4

theorem ofMatroid_lt_iff {M M' : Matroid α} : Matroidᵣ.ofMatroid M < Matroidᵣ.ofMatroid M' ↔ M <r M' := by simp

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

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

Разделы

Аффилиация

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