instFintypeSymbol — Mathlib

English

If T and N are finite types, then Symbol T N is a finite type; there is a finite type instance for Symbol T N.

Русский

Если T и N — конечные множества, то Symbol T N является конечного типа; существует инстанс конечного типа для Symbol T N.

LaTeX

$$Fintype\\, (Symbol\\ T\\ N)$$

Lean4

instance {T✝} {N✝} [Fintype✝ T✝] [Fintype✝ N✝] : Fintype✝¹ (@Symbol✝ T✝ N✝) :=
  derive_fintype% _

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