Type class for finitely enumerable types. The property is stronger
than Fintype
in that it assigns each element a rank in a finite
enumeration.
FinEnum α
means that α
is finite and can be enumerated in some order,
i.e. α
has an explicit bijection with Fin n
for some n.
- card : ℕ
FinEnum.card
is the cardinality of theFinEnum
- equiv : α ≃ Fin (FinEnum.card α)
- decEq : DecidableEq α
Instances
transport a FinEnum
instance across an equivalence
Equations
- FinEnum.ofEquiv α h = FinEnum.mk (FinEnum.card α) (h.trans FinEnum.equiv)
Instances For
create a FinEnum
instance from an exhaustive list without duplicates
Equations
- FinEnum.ofNodupList xs h h' = FinEnum.mk xs.length { toFun := fun (x : α) => ⟨List.indexOf x xs, ⋯⟩, invFun := xs.get, left_inv := ⋯, right_inv := ⋯ }
Instances For
create a FinEnum
instance from an exhaustive list; duplicates are removed
Equations
- FinEnum.ofList xs h = FinEnum.ofNodupList xs.dedup ⋯ ⋯
Instances For
create an exhaustive list of the values of a given type
Equations
- FinEnum.toList α = List.map (⇑FinEnum.equiv.symm) (List.finRange (FinEnum.card α))
Instances For
create a FinEnum
instance using a surjection
Equations
- FinEnum.ofSurjective f h = FinEnum.ofList (List.map f (FinEnum.toList β)) ⋯
Instances For
create a FinEnum
instance using an injection
Equations
- FinEnum.ofInjective f h = FinEnum.ofList (List.filterMap (Function.partialInv f) (FinEnum.toList β)) ⋯
Instances For
Equations
Equations
Equations
Equations
- FinEnum.prod = FinEnum.ofList (FinEnum.toList α ×ˢ FinEnum.toList β) ⋯
Equations
- FinEnum.sum = FinEnum.ofList (List.map Sum.inl (FinEnum.toList α) ++ List.map Sum.inr (FinEnum.toList β)) ⋯
Equations
- FinEnum.fin = FinEnum.ofList (List.finRange n) ⋯
Equations
- FinEnum.Quotient.enum s = FinEnum.ofSurjective Quotient.mk'' ⋯
enumerate all finite sets of a given type
Equations
- FinEnum.Finset.enum [] = [∅]
- FinEnum.Finset.enum (x_1 :: xs) = do let r ← FinEnum.Finset.enum xs [r, {x_1} ∪ r]
Instances For
Equations
- FinEnum.Finset.finEnum = FinEnum.ofList (FinEnum.Finset.enum (FinEnum.toList α)) ⋯
Equations
- FinEnum.Subtype.finEnum p = FinEnum.ofList (List.filterMap (fun (x : α) => if h : p x then some ⟨x, h⟩ else none) (FinEnum.toList α)) ⋯
Equations
- FinEnum.instSigma β = FinEnum.ofList ((FinEnum.toList α).bind fun (a : α) => List.map (Sigma.mk a) (FinEnum.toList (β a))) ⋯
Equations
- FinEnum.PSigma.finEnum = FinEnum.ofEquiv ((i : α) × β i) (Equiv.psigmaEquivSigma β)
Equations
- FinEnum.PSigma.finEnumPropLeft = if h : α then FinEnum.ofList (List.map (PSigma.mk h) (FinEnum.toList (β h))) ⋯ else FinEnum.ofList [] ⋯
Equations
- FinEnum.PSigma.finEnumPropProp = if h : ∃ (a : α), β a then FinEnum.ofList [⟨⋯, ⋯⟩] ⋯ else FinEnum.ofList [] ⋯
Equations
- FinEnum.instSubtypeMemListOfDecidableEq xs = FinEnum.ofList xs.attach ⋯
Equations
- FinEnum.instFintype = { elems := Finset.map FinEnum.equiv.symm.toEmbedding Finset.univ, complete := ⋯ }
enumerate all functions whose domain and range are finitely enumerable
Equations
- List.Pi.enum β = List.map (fun (f : (i : α) → i ∈ FinEnum.toList α → β i) (x : α) => f x ⋯) ((FinEnum.toList α).pi fun (x : α) => FinEnum.toList (β x))
Instances For
Equations
- List.Pi.finEnum = FinEnum.ofList (List.Pi.enum β) ⋯
Equations
- List.pfunFinEnum p α = if hp : p then FinEnum.ofList (List.map (fun (x : α hp) (x_1 : p) => x) (FinEnum.toList (α hp))) ⋯ else FinEnum.ofList [fun (hp' : p) => ⋯.elim] ⋯