instPartialOrder

Mathlib.Combinatorics.Matroid.Minor.Order

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

Lean4

/-- The minor order is a `PartialOrder` on `Matroid α`.
We prefer the spelling `N ≤m M` over `N ≤ M` for the dot notation. -/
instance (α : Type*) : PartialOrder (Matroid α) where
  le N M := N ≤m M
  lt N M := N <m M
  le_refl _ := IsMinor.refl
  le_trans _ _ _ := IsMinor.trans
  le_antisymm _ _ := IsMinor.antisymm

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

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

Разделы

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

Аффилиация

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