mkOfLe_refl — Mathlib

English

Let n be a natural number and j an index in the (n+1)-point simplex. The morphism obtained by applying mkOfLe to the same index (j, j) is equal to the 1-simplex constant at j, viewed as a map to the n-simplex Δ^n.

Русский

Пусть n — натуральное число, а j — индекс в множестве Fin(n+1). Морфизм mkOfLe, применённый к паре (j, j), равен константному ребру Δ^1, направленному в Δ^n и фиксирующему вершину j.

LaTeX

$$$mkOfLe\, j\, j = (\langle 1 \rangle).const(\langle n \rangle)\, j$$$

Lean4

@[simp]
theorem mkOfLe_refl {n} (j : Fin (n + 1)) : mkOfLe j j (by cutsat) = ⦋1⦌.const ⦋n⦌ j :=
  Hom.ext_one_left _ _

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