instFintypeSignType — Mathlib

English

SignType is a finite type; its elements can be enumerated by enumList.

Русский

SignType является конечным типом; его элементы можно перечислить через enumList.

LaTeX

$$$|SignType| = 3$$$

Lean4

instance : Fintype✝ SignType
    where
  elems✝ := Finset.mk✝ SignType.enumList SignType.enumList_nodup
  complete✝ := by
    intro x✝
    rw [Finset.mem_mk✝, Multiset.mem_coe✝, List.mem_iff_getElem?✝]
    exact ⟨SignType.ctorIdx x✝, SignType.enumList_getElem?_ctorIdx_eq x✝⟩

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