instFintype — Mathlib

English

For a multicospan shape J with finite left and right parts, the walking multicospan category is finite.

Русский

Для формы multicospan с конечными левой и правой частями существуются конечные ходовая multicospan и соответствующая структура.

LaTeX

$$$\text{FinCat}(\mathrm{WalkingMultispan}(J)) \quad\text{if } [\text{Fintype } J.L] \land [\text{Fintype } J.R]$$$

Lean4

instance : Fintype (WalkingMultispan J) :=
  .ofEquiv _ (proxy_equiv% (WalkingMultispan J))

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