Structures · Data types
FinEnum
FinEnum α means that α is finite and can be enumerated in some order,
i.e. α has an explicit bijection with Fin n for some n.
- Defined in
- Mathlib.Data.FinEnum
- Shape
- One type argument · adds card, equiv, decEq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every FinEnum is also a
Concrete types that are instances22
- BitVec
- UInt64
- UInt8
- UInt16
- UInt32
- Int32
- Int8
- Int64
- Int16
- Empty
- PEmpty
- Subtype
- Prod
- ULift
- Fin
- PUnit
- Sum
- Sigma
- Finset
- Option
- Quotient
- PSigma
How is a type an instance?
Loading the hierarchy index…
Assumed by44
- FinEnum.card
- FinEnum.equiv
- FinEnum.card_eq_fintypeCard
- FinEnum.toList
- FinEnum.recEmptyOption
- FinEnum.insertNone
- FinEnum.recEmptyOption.eq_def
- List.Pi.enum
- FinEnum.card_pos_iff
- FinEnum.card_pos
- List.mem_pi_toList
- FinEnum.mem_toList
- FinEnum.card_eq_zero_iff
- FinEnum.card_eq_zero
- FinEnum.card_fin
- FinEnum.recEmptyOption_of_card_pos
- FinEnum.PSigma.finEnumPropRight
- FinEnum.instFintype
- FinEnum.nodup_toList
- FinEnum.Quotient.enum
- FinEnum.down_equiv_symm
- FinEnum.equiv_down
- FinEnum.recEmptyOption_of_card_eq_zero
- ULift.instFinEnum
- FinEnum.card_eq_one
- FinEnum.instSigma
- FinEnum.Subtype.finEnum
- List.Pi.mem_enum
- List.Pi.finEnum
- FinEnum.PSigma.finEnumPropLeft
- FinEnum.card_ulift
- FinEnum.PSigma.finEnum
- FinEnum.prod
- FinEnum.instFinEnumOptionLast
- FinEnum.ofEquiv
- FinEnum.Finset.finEnum
- List.pfunFinEnum
- FinEnum.up_equiv_symm
- FinEnum.sum
- FinEnum.equiv_up
- FinEnum.card_ne_zero
- FinEnum.ofSurjective
- FinEnum.decEq
- FinEnum.ofInjective