hom_zero_zero — Mathlib

English

Any morphism f: Δ^0 → Δ^0 is equal to the identity on Δ^0; hence the zero morphism equals the identity by subsingleton.

Русский

Любой морфизм f: Δ^0 → Δ^0 равен тождественному на Δ^0; следовательно нулевой морфизм равен тождественному, поскольку множество морфизмов — одиничное.

LaTeX

$$∀ f: Δ^0 ⟶ Δ^0, f = id_{Δ^0}$$

Lean4

theorem hom_zero_zero (f : ⦋0⦌ ⟶ ⦋0⦌) : f = 𝟙 _ := by apply Subsingleton.elim

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