Documentation

Mathlib.Data.Fintype.Basic

Instances for finite types #

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

@[implicit_reducible]

instance Fin.fintype (n : ℕ) :

Fintype (Fin n)

theorem Fin.univ_def (n : ℕ) :

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

theorem Finset.univ_fin2 :

univ = {0, 1}

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

theorem Fin.eq_iff_eq_zero_iff (a b : Fin 2) :

a = b ↔ (a = 0 ↔ b = 0)

@[implicit_reducible]

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

@[implicit_reducible]

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.

@[implicit_reducible]

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 = ∅

@[implicit_reducible]

instance Unit.fintype :

theorem Fintype.univ_unit :

Finset.univ = {()}

@[implicit_reducible]

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}

@[implicit_reducible]

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

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

Instances For

@[implicit_reducible]

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

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

Instances For

@[implicit_reducible]

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

Fintype (ULift.{u_5, u_4} α)

@[implicit_reducible]

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

Fintype (PLift α)

@[implicit_reducible]

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

Fintype (PLift p)

@[implicit_reducible]

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

Fintype (Quotient s)

@[implicit_reducible]

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

Fintype ((a : α) ×' β a)

@[implicit_reducible]

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

Fintype ((a : α) ×' β a)

@[implicit_reducible]

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

Fintype ((a : α) ×' β a)

@[implicit_reducible]

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 α.

Instances For

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

A Nonempty Fintype constructively contains an element.

Instances For

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.

Instances For

@[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.

Instances For

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) [Std.Symm 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.