discreteHomFintype — Mathlib

English

In the discrete category on α, every hom-set is finite: for any X,Y : Discrete α, the hom-set X ⟶ Y is finite.

Русский

В дискретной категории на α каждая пара объектов имеет конечное множество морфизмов, т.е. X ⟶ Y конечно.

LaTeX

$$$\\forall X,Y : \\operatorname{Discrete}(\\alpha), \\operatorname{Fintype}(X \\to Y).$$$

Lean4

instance discreteHomFintype {α : Type*} (X Y : Discrete α) : Fintype (X ⟶ Y) := by classical apply ULift.fintype

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