Instances for finite types

This file is a collection of basic Fintype instances for types such as Fin, Prod and pi types.

instance Fin.fintype (n : ℕ) : Fintype (Fin n)

theorem Fin.univ_def (n : ℕ) : Finset.univ = { val := ↑(List.finRange n), nodup := ⋯ }

theorem Finset.val_univ_fin (n : ℕ) : univ.val = ↑(List.finRange n)

theorem nonempty_fintype (α : Type u_4) [Finite α] : Nonempty (Fintype α)

See also nonempty_encodable, nonempty_denumerable.

@[simp]

theorem List.toFinset_finRange (n : ℕ) : (finRange n).toFinset = Finset.univ

@[simp]

theorem Fin.univ_val_map {α : Type u_1} {n : ℕ} (f : Fin n → α) : Multiset.map f Finset.univ.val = ↑(List.ofFn f)

theorem Fin.univ_image_def {α : Type u_1} {n : ℕ} [DecidableEq α] (f : Fin n → α) : Finset.image f Finset.univ = (List.ofFn f).toFinset

theorem Fin.univ_map_def {α : Type u_1} {n : ℕ} (f : Fin n ↪ α) : Finset.map f Finset.univ = { val := ↑(List.ofFn ⇑f), nodup := ⋯ }

@[simp]

theorem Fin.image_succAbove_univ {n : ℕ} (i : Fin (n + 1)) : Finset.image i.succAbove Finset.univ = {i}ᶜ

@[simp]

theorem Fin.image_succ_univ (n : ℕ) : Finset.image succ Finset.univ = {0}ᶜ

@[simp]

theorem Fin.image_castSucc (n : ℕ) : Finset.image castSucc Finset.univ = {last n}ᶜ

theorem Fin.univ_succ (n : ℕ) : Finset.univ = Finset.cons 0 (Finset.map { toFun := succ, inj' := ⋯ } Finset.univ) ⋯

Embed Fin n into Fin (n + 1) by prepending zero to the univ

theorem Fin.univ_castSuccEmb (n : ℕ) : Finset.univ = Finset.cons (last n) (Finset.map castSuccEmb Finset.univ) ⋯

Embed Fin n into Fin (n + 1) by appending a new Fin.last n to the univ

theorem Fin.univ_succAbove (n : ℕ) (p : Fin (n + 1)) : Finset.univ = Finset.cons p (Finset.map p.succAboveEmb Finset.univ) ⋯

Embed Fin n into Fin (n + 1) by inserting around a specified pivot p : Fin (n + 1) into the univ

@[simp]

theorem Fin.univ_image_get {α : Type u_1} [DecidableEq α] (l : List α) : Finset.image l.get Finset.univ = l.toFinset

@[simp]

theorem Fin.univ_image_getElem' {α : Type u_1} {β : Type u_2} [DecidableEq β] (l : List α) (f : α → β) : Finset.image (fun (i : Fin l.length) => f l[↑i]) Finset.univ = (List.map f l).toFinset

theorem Fin.univ_image_get' {α : Type u_1} {β : Type u_2} [DecidableEq β] (l : List α) (f : α → β) : Finset.image (fun (x : Fin l.length) => f (l.get x)) Finset.univ = (List.map f l).toFinset

instance Unique.fintype {α : Type u_4} [Unique α] : Fintype α

instance Fintype.subtypeEq {α : Type u_1} (y : α) : Fintype { x : α // x = y }

Short-circuit instance to decrease search for Unique.fintype, since that relies on a subsingleton elimination for Unique.

instance Fintype.subtypeEq' {α : Type u_1} (y : α) : Fintype { x : α // y = x }

Short-circuit instance to decrease search for Unique.fintype, since that relies on a subsingleton elimination for Unique.

theorem Fintype.univ_empty : Finset.univ = ∅

theorem Fintype.univ_pempty : Finset.univ = ∅

instance Unit.fintype : Fintype Unit

theorem Fintype.univ_unit : Finset.univ = {()}

instance PUnit.fintype : Fintype PUnit.{u_4 + 1}

theorem Fintype.univ_punit : Finset.univ = {PUnit.unit}

@[simp]

theorem Fintype.univ_bool : Finset.univ = {true, false}

def Fintype.prodLeft {α : Type u_4} {β : Type u_5} [DecidableEq α] [Fintype (α × β)] [Nonempty β] : Fintype α

Given that α × β is a fintype, α is also a fintype.

def Fintype.prodRight {α : Type u_4} {β : Type u_5} [DecidableEq β] [Fintype (α × β)] [Nonempty α] : Fintype β

Given that α × β is a fintype, β is also a fintype.

instance ULift.fintype (α : Type u_4) [Fintype α] : Fintype (ULift.{u_5, u_4} α)

instance PLift.fintype (α : Type u_4) [Fintype α] : Fintype (PLift α)

instance PLift.fintypeProp (p : Prop) [Decidable p] : Fintype (PLift p)

instance Quotient.fintype {α : Type u_1} [Fintype α] (s : Setoid α) [DecidableRel fun (x1 x2 : α) => x1 ≈ x2] : Fintype (Quotient s)

instance PSigma.fintypePropLeft {α : Prop} {β : α → Type u_4} [Decidable α] [(a : α) → Fintype (β a)] : Fintype ((a : α) ×' β a)

instance PSigma.fintypePropRight {α : Type u_4} {β : α → Prop} [(a : α) → Decidable (β a)] [Fintype α] : Fintype ((a : α) ×' β a)

instance PSigma.fintypePropProp {α : Prop} {β : α → Prop} [Decidable α] [(a : α) → Decidable (β a)] : Fintype ((a : α) ×' β a)

instance pfunFintype (p : Prop) [Decidable p] (α : p → Type u_4) [(hp : p) → Fintype (α hp)] : Fintype ((hp : p) → α hp)

def truncOfMultisetExistsMem {α : Type u_4} (s : Multiset α) : (∃ (x : α), x ∈ s) → Trunc α

For s : Multiset α, we can lift the existential statement that ∃ x, x ∈ s to a Trunc α.

def truncOfNonemptyFintype (α : Type u_4) [Nonempty α] [Fintype α] : Trunc α

A Nonempty Fintype constructively contains an element.

def truncSigmaOfExists {α : Type u_4} [Fintype α] {P : α → Prop} [DecidablePred P] (h : ∃ (a : α), P a) : Trunc ((a : α) ×' P a)

By iterating over the elements of a fintype, we can lift an existential statement ∃ a, P a to Trunc (Σ' a, P a), containing data.

@[simp]

theorem Multiset.count_univ {α : Type u_1} [Fintype α] [DecidableEq α] (a : α) : count a Finset.univ.val = 1

@[simp]

theorem Multiset.map_univ_val_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α ≃ β) : map (⇑e) Finset.univ.val = Finset.univ.val

@[simp]

theorem Multiset.bijective_iff_map_univ_eq_univ {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) : Function.Bijective f ↔ map f Finset.univ.val = Finset.univ.val

For functions on finite sets, they are bijections iff they map universes into universes.

@[irreducible]

noncomputable def seqOfForallFinsetExistsAux {α : Type u_4} [DecidableEq α] (P : α → Prop) (r : α → α → Prop) (h : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y) : ℕ → α

Auxiliary definition to show exists_seq_of_forall_finset_exists.

theorem exists_seq_of_forall_finset_exists {α : Type u_4} (P : α → Prop) (r : α → α → Prop) (h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y) : ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Induction principle to build a sequence, by adding one point at a time satisfying a given relation with respect to all the previously chosen points.

More precisely, Assume that, for any finite set s, one can find another point satisfying some relation r with respect to all the points in s. Then one may construct a function f : ℕ → α such that r (f m) (f n) holds whenever m < n. We also ensure that all constructed points satisfy a given predicate P.

theorem exists_seq_of_forall_finset_exists' {α : Type u_4} (P : α → Prop) (r : α → α → Prop) [IsSymm α r] (h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y) : ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ Pairwise (Function.onFun r f)

Induction principle to build a sequence, by adding one point at a time satisfying a given symmetric relation with respect to all the previously chosen points.

More precisely, Assume that, for any finite set s, one can find another point satisfying some relation r with respect to all the points in s. Then one may construct a function f : ℕ → α such that r (f m) (f n) holds whenever m ≠ n. We also ensure that all constructed points satisfy a given predicate P.