subsingleton_hom — Mathlib

English

For a preorder X, any two morphisms X ⟶ Y in the preorder category coincide; the hom-set is a subsingleton.

Русский

Для преордера X множество морфизмов X ⟶ Y в соответствующей категории является одноэлементным.

LaTeX

$$$\text{Subsingleton }( (\text{Preorder.smallCategory } α).\mathrm{Hom}\ U\ V ).$$$

Lean4

instance subsingleton_hom {α : Type u} [Preorder α] (U V : α) : Subsingleton (U ⟶ V) :=
  ⟨fun _ _ => ULift.ext _ _ (Subsingleton.elim _ _)⟩

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