trans

Mathlib.Combinatorics.Matroid.Minor.Restrict

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

English

If M₁ ≤r M₂ and M₂ ≤r M₃, then M₁ ≤r M₃.

Русский

Если M₁ ≤r M₂ и M₂ ≤r M₃, то M₁ ≤r M₃.

LaTeX

$$$ M_1 \\le_r M_2 \\land M_2 \\le_r M_3 \\Rightarrow M_1 \\le_r M_3 $$$

Lean4

theorem trans {M₁ M₂ M₃ : Matroid α} (h : M₁ ≤r M₂) (h' : M₂ ≤r M₃) : M₁ ≤r M₃ :=
  le_trans (α := Matroidᵣ α) h h'

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

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

Разделы

Аффилиация

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