const_fac_thru_zero — Mathlib

English

A constant morphism factors through the zero object: const x y i = const x ⦋0⦌ 0 ≫ SimplexCategory.const ⦋0⦌ m i.

Русский

Константный морфизм факторизуется через нулевой объект: const x y i = const x ⟦0⟧ 0 ∘ SimplexCategory.const ⟦0⟧ m i.

LaTeX

$$$\\text{const } x y i = \\text{const } x(\\langle0\\rangle) 0 \\circ \\text{SimplexCategory.const}(\\langle0\\rangle) m i$.$$

Lean4

theorem const_fac_thru_zero (n m : SimplexCategory) (i : Fin (m.len + 1)) :
    const n m i = const n ⦋0⦌ 0 ≫ SimplexCategory.const ⦋0⦌ m i := by rw [const_comp]; rfl

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