subsingleton2Hom — Mathlib

English

In LocallyDiscrete C, for any a,b, and any f,g : a ⟶ b, the hom-set from f to g is a Subsingleton.

Русский

В LocallyDiscrete C для любых объектов a,b и любых f,g: a ⟶ b, множество гомоморфизмов от f к g одноэлементно.

LaTeX

$$$\\forall C, [\\text{Category } C], \\forall a,b:\\text{LocallyDiscrete } C, \\forall f,g:\\, a\\to b, \\operatorname{Subsingleton}((f\\to g)).$$$

Lean4

/-- This instance is used to see through the synonym `a ⟶ b = Discrete (a.as ⟶ b.as)`. -/
instance subsingleton2Hom {a b : LocallyDiscrete C} (f g : a ⟶ b) : Subsingleton (f ⟶ g) :=
  instSubsingletonDiscreteHom f g

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