congr_toOrderHom_apply — Mathlib

English

Same idea as congr_toOrderHom_apply: equality of morphisms implies equality of their order-homomorphisms on all indices.

Русский

Та же идея, что и выше: равенство морфизмов влечёт равенство их гомоморфизмов порядка на всех индексах.

LaTeX

$$$\\forall {a,b:\\, SimplexCategory} {f,g:\\, a \\to b},\\; f=g \\Rightarrow\\; \\forall x,\\; f.toOrderHom x = g.toOrderHom x.$$$

Lean4

theorem congr_toOrderHom_apply {a b : SimplexCategory} {f g : a ⟶ b} (h : f = g) (x : Fin (a.len + 1)) :
    f.toOrderHom x = g.toOrderHom x := by rw [h]

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