coe_triangle_down_toOrderHom — Mathlib

English

The downward projection of the triangle yields the 3-term vector [a,b,c], i.e., the order-preserving map sending 0↦a, 1↦b, 2↦c.

Русский

Опускание треугольника даёт тройку вершин a,b,c как порядокобразующее отображение 0↦a, 1↦b, 2↦c.

LaTeX

$$$\\uparrow(triangle(a,b,c,hab,hbc)).down.toOrderHom = ![a,b,c]$$$

Lean4

theorem coe_triangle_down_toOrderHom {n : ℕ} (a b c : Fin (n + 1)) (hab : a ≤ b) (hbc : b ≤ c) :
    ↑(triangle a b c hab hbc).down.toOrderHom = ![a, b, c] :=
  rfl

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