instFintypeWalkingParallelPairHom

English

For any j, j' in WalkingParallelPair, the type of morphisms between them is finite.

Русский

Для любых j, j' в WalkingParallelPair множество морфизмов между ними конечно.

LaTeX

$$$\#\operatorname{Hom}_{\mathrm{WalkingParallelPair}}(j, j') < \infty$$$

Lean4

instance instFintypeWalkingParallelPairHom (j j' : WalkingParallelPair) : Fintype (WalkingParallelPairHom j j')
    where
  elems :=
    WalkingParallelPair.recOn j
      (WalkingParallelPair.recOn j' [WalkingParallelPairHom.id zero].toFinset [left, right].toFinset)
      (WalkingParallelPair.recOn j' ∅ [WalkingParallelPairHom.id one].toFinset)
  complete := by aesop

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