ext₀ — Mathlib

English

Two morphisms f,g: X ⟶ Δ[0] are equal since Δ[0] is terminal and there is a unique morphism to it.

Русский

Два морфизма f,g: X → Δ[0] равны, потому что Δ[0] является терминальным объектом и существует единственный морфизм в него.

LaTeX

$$$ \forall f,g: X \to Δ[0], f = g $$$

Lean4

@[ext]
theorem ext₀ {X : SSet.{u}} {f g : X ⟶ Δ[0]} : f = g :=
  isTerminalObj₀.hom_ext _ _

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