mkOfLe — Mathlib

English

Given i ≤ j in Fin(n+1), there is a morphism ⦋1⦌ ⟶ ⦋n⦌ that selects indices i and j, defining a standard sub-interval inclusion.

Русский

Для i ≤ j в Fin(n+1) существует морфизм ⦋1⦌ ⟶ ⦋n⦌, выбирающий индексы i и j, задающий стандартное включение подпериода.

LaTeX

$$$\\text{mkOfLe}(i,j,h) : ⦋1⦌ ⟶ ⦋n⦌$$$

Lean4

/-- The morphism `⦋1⦌ ⟶ ⦋n⦌` that picks out a specified `h : i ≤ j` in `Fin (n+1)`. -/
def mkOfLe {n} (i j : Fin (n + 1)) (h : i ≤ j) : ⦋1⦌ ⟶ ⦋n⦌ :=
  SimplexCategory.mkHom
    { toFun := fun
        | 0 => i
        | 1 => j
      monotone' := fun
        | 0, 0, _ | 1, 1, _ => le_rfl
        | 0, 1, _ => h }

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