Type class for finitely enumerable types. The property is stronger
than fintype in that it assigns each element a rank in a finite
enumeration.
@[class]
- card : ℕ
- equiv : α ≃ fin (fin_enum.card α)
- dec_eq : decidable_eq α
fin_enum α means that α is finite and can be enumerated in some order,
i.e. α has an explicit bijection with fin n for some n.
Instances
- fin_enum.pempty
- fin_enum.empty
- fin_enum.punit
- fin_enum.prod
- fin_enum.sum
- fin_enum.fin
- fin_enum.quotient.enum
- fin_enum.finset.fin_enum
- fin_enum.subtype.fin_enum
- fin_enum.fin_enum
- fin_enum.psigma.fin_enum
- fin_enum.psigma.fin_enum_prop_left
- fin_enum.psigma.fin_enum_prop_right
- fin_enum.psigma.fin_enum_prop_prop
- fin_enum.pi.fin_enum
- fin_enum.pfun_fin_enum
transport a fin_enum instance across an equivalence
Equations
- fin_enum.of_equiv α h = fin_enum.mk (fin_enum.card α) (h.trans (fin_enum.equiv α))
create a fin_enum instance from an exhaustive list without duplicates
create a fin_enum instance from an exhaustive list; duplicates are removed
Equations
- fin_enum.of_list xs h = fin_enum.of_nodup_list xs.erase_dup _ _
create an exhaustive list of the values of a given type
Equations
- fin_enum.to_list α = list.map ⇑((fin_enum.equiv α).symm) (list.fin_range (fin_enum.card α))
@[simp]
@[simp]
def
fin_enum.of_surjective
{α : Type u_1}
{β : Type u_2}
(f : β → α)
[decidable_eq α]
[fin_enum β] :
function.surjective f → fin_enum α
create a fin_enum instance using a surjection
Equations
- fin_enum.of_surjective f h = fin_enum.of_list (list.map f (fin_enum.to_list β)) _
def
fin_enum.of_injective
{α : Type u_1}
{β : Type u_2}
(f : α → β)
[decidable_eq α]
[fin_enum β] :
function.injective f → fin_enum α
create a fin_enum instance using an injection
Equations
@[instance]
Equations
- fin_enum.pempty = fin_enum.of_list list.nil fin_enum.pempty._proof_1
@[instance]
Equations
- fin_enum.empty = fin_enum.of_list list.nil fin_enum.empty._proof_1
@[instance]
Equations
- fin_enum.punit = fin_enum.of_list [punit.star] fin_enum.punit._proof_1
@[instance]
Equations
- fin_enum.prod = fin_enum.of_list ((fin_enum.to_list α).product (fin_enum.to_list β)) fin_enum.prod._proof_1
@[instance]
Equations
- fin_enum.sum = fin_enum.of_list (list.map sum.inl (fin_enum.to_list α) ++ list.map sum.inr (fin_enum.to_list β)) fin_enum.sum._proof_1
@[instance]
Equations
- fin_enum.fin = fin_enum.of_list (list.fin_range n) fin_enum.fin._proof_1
@[instance]
def
fin_enum.quotient.enum
{α : Type u_1}
[fin_enum α]
(s : setoid α)
[decidable_rel has_equiv.equiv] :
Equations
enumerate all finite sets of a given type
Equations
- fin_enum.finset.enum (x :: xs) = fin_enum.finset.enum xs >>= λ (r : finset α), [r, {x} ∪ r]
- fin_enum.finset.enum list.nil = [∅]
@[simp]
theorem
fin_enum.finset.mem_enum
{α : Type u_1}
[decidable_eq α]
(s : finset α)
(xs : list α) :
s ∈ fin_enum.finset.enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs
@[instance]
Equations
- fin_enum.finset.fin_enum = fin_enum.of_list (fin_enum.finset.enum (fin_enum.to_list α)) fin_enum.finset.fin_enum._proof_1
@[instance]
def
fin_enum.subtype.fin_enum
{α : Type u_1}
[fin_enum α]
(p : α → Prop)
[decidable_pred p] :
fin_enum {x // p x}
Equations
- fin_enum.subtype.fin_enum p = fin_enum.of_list (list.filter_map (λ (x : α), dite (p x) (λ (h : p x), option.some ⟨x, h⟩) (λ (h : ¬p x), option.none)) (fin_enum.to_list α)) _
@[instance]
Equations
- fin_enum.fin_enum β = fin_enum.of_list ((fin_enum.to_list α).bind (λ (a : α), list.map (sigma.mk a) (fin_enum.to_list (β a)))) _
@[instance]
def
fin_enum.psigma.fin_enum
{α : Type u_1}
{β : α → Type u_2}
[fin_enum α]
[Π (a : α), fin_enum (β a)] :
fin_enum (Σ' (a : α), β a)
Equations
- fin_enum.psigma.fin_enum = fin_enum.of_equiv (Σ (i : α), β i) (equiv.psigma_equiv_sigma (λ (a : α), β a))
@[instance]
def
fin_enum.psigma.fin_enum_prop_left
{α : Prop}
{β : α → Type u_1}
[Π (a : α), fin_enum (β a)]
[decidable α] :
fin_enum (Σ' (a : α), β a)
Equations
- fin_enum.psigma.fin_enum_prop_left = dite α (λ (h : α), fin_enum.of_list (list.map (psigma.mk h) (fin_enum.to_list (β h))) _) (λ (h : ¬α), fin_enum.of_list list.nil _)
@[instance]
def
fin_enum.psigma.fin_enum_prop_right
{α : Type u_1}
{β : α → Prop}
[fin_enum α]
[Π (a : α), decidable (β a)] :
fin_enum (Σ' (a : α), β a)
Equations
- fin_enum.psigma.fin_enum_prop_right = fin_enum.of_equiv {a // β a} {to_fun := λ (_x : Σ' (a : α), β a), fin_enum.psigma.fin_enum_prop_right._match_1 _x, inv_fun := λ (_x : {a // β a}), fin_enum.psigma.fin_enum_prop_right._match_2 _x, left_inv := _, right_inv := _}
- fin_enum.psigma.fin_enum_prop_right._match_1 ⟨x, y⟩ = ⟨x, y⟩
- fin_enum.psigma.fin_enum_prop_right._match_2 ⟨x, y⟩ = ⟨x, y⟩
@[instance]
def
fin_enum.psigma.fin_enum_prop_prop
{α : Prop}
{β : α → Prop}
[decidable α]
[Π (a : α), decidable (β a)] :
fin_enum (Σ' (a : α), β a)
Equations
- fin_enum.psigma.fin_enum_prop_prop = dite (∃ (a : α), β a) (λ (h : ∃ (a : α), β a), fin_enum.of_list [⟨_, _⟩] _) (λ (h : ¬∃ (a : α), β a), fin_enum.of_list list.nil _)
@[instance]
Equations
- fin_enum.fintype = {elems := finset.map (fin_enum.equiv α).symm.to_embedding finset.univ, complete := _}
def
fin_enum.pi.cons
{α : Type u_1}
{β : α → Type u_2}
[decidable_eq α]
(x : α)
(xs : list α)
(y : β x)
(f : Π (a : α), a ∈ xs → β a)
(a : α) :
For pi.cons x xs y f create a function where every i ∈ xs is mapped to f i and
x is mapped to y
def
fin_enum.pi.tail
{α : Type u_1}
{β : α → Type u_2}
{x : α}
{xs : list α}
(f : Π (a : α), a ∈ x :: xs → β a)
(a : α) :
a ∈ xs → β a
Given f a function whose domain is x :: xs, produce a function whose domain
is restricted to xs.
Equations
- fin_enum.pi.tail f a h = f a _
pi xs f creates the list of functions g such that, for x ∈ xs, g x ∈ f x
Equations
- fin_enum.pi (x :: xs) fs = fin_enum.pi.cons x xs <$> fs x <*> fin_enum.pi xs fs
- fin_enum.pi list.nil fs = [λ (x : α) (h : x ∈ list.nil), false.elim h]
theorem
fin_enum.mem_pi
{α : Type u_1}
{β : α → Type (max u_1 u_2)}
[fin_enum α]
[Π (a : α), fin_enum (β a)]
(xs : list α)
(f : Π (a : α), a ∈ xs → β a) :
f ∈ fin_enum.pi xs (λ (x : α), fin_enum.to_list (β x))
def
fin_enum.pi.enum
{α : Type u_1}
(β : α → Type (max u_1 u_2))
[fin_enum α]
[Π (a : α), fin_enum (β a)] :
list (Π (a : α), β a)
enumerate all functions whose domain and range are finitely enumerable
Equations
- fin_enum.pi.enum β = list.map (λ (f : Π (a : α), a ∈ fin_enum.to_list α → β a) (x : α), f x _) (fin_enum.pi (fin_enum.to_list α) (λ (x : α), fin_enum.to_list (β x)))
theorem
fin_enum.pi.mem_enum
{α : Type u_1}
{β : α → Type (max u_1 u_2)}
[fin_enum α]
[Π (a : α), fin_enum (β a)]
(f : Π (a : α), β a) :
f ∈ fin_enum.pi.enum β
@[instance]
def
fin_enum.pi.fin_enum
{α : Type u_1}
{β : α → Type (max u_1 u_2)}
[fin_enum α]
[Π (a : α), fin_enum (β a)] :
fin_enum (Π (a : α), β a)
Equations
- fin_enum.pi.fin_enum = fin_enum.of_list (fin_enum.pi.enum (λ (a : α), β a)) fin_enum.pi.fin_enum._proof_1
@[instance]
def
fin_enum.pfun_fin_enum
(p : Prop)
[decidable p]
(α : p → Type u_1)
[Π (hp : p), fin_enum (α hp)] :
fin_enum (Π (hp : p), α hp)
Equations
- fin_enum.pfun_fin_enum p α = dite p (λ (hp : p), fin_enum.of_list (list.map (λ (x : α hp) (hp' : p), x) (fin_enum.to_list (α hp))) _) (λ (hp : ¬p), fin_enum.of_list [λ (hp' : p), _.elim] _)