coe_map — Mathlib

English

The underlying linear order hom of the mapped morphism equals the order-hom associated to f.

Русский

Линейный отображение порядка стянутого отображения совпадает с отображением порядка от f.

LaTeX

$$$\\uparrow(\\text{skeletalFunctor.map } f).hom = f.toOrderHom$$$

Lean4

theorem coe_map {Δ₁ Δ₂ : SimplexCategory} (f : Δ₁ ⟶ Δ₂) : ↑(skeletalFunctor.map f).hom = f.toOrderHom :=
  rfl

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