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✝⟩