Finite types

This file defines a typeclass to state that a type is finite.

Main declarations

• Fintype α: Typeclass saying that a type is finite. It takes as fields a Finset and a proof that all terms of type α are in it.
• Finset.univ: The finset of all elements of a fintype.

See Data.Fintype.Card for the cardinality of a fintype, the equivalence with Fin (Fintype.card α), and pigeonhole principles.

Instances

Instances for Fintype for

• {x // p x} are in this file as Fintype.subtype
• Option α are in Data.Fintype.Option
• α × β are in Data.Fintype.Prod
• α ⊕ β are in Data.Fintype.Sum
• Σ (a : α), β a are in Data.Fintype.Sigma

These files also contain appropriate Infinite instances for these types.

Infinite instances for ℕ, ℤ, Multiset α, and List α are in Data.Fintype.Lattice.

Types which have a surjection from/an injection to a Fintype are themselves fintypes. See Fintype.ofInjective and Fintype.ofSurjective.

class Fintype (α : Type u_4) : Type u_4

Fintype α means that α is finite, i.e. there are only finitely many distinct elements of type α. The evidence of this is a finset elems (a list up to permutation without duplicates), together with a proof that everything of type α is in the list.

• elems : Finset α

  The Finset containing all elements of a Fintype

• complete : ∀ (x : α), x ∈ Fintype.elems

  A proof that elems contains every element of the type

Instances

• Additive.fintype
• Bool.fintype
• CategoryTheory.FinCategory.instFintypeHomObjAsType
• CategoryTheory.Limits.WidePullbackShape.fintypeHom
• CategoryTheory.Limits.WidePullbackShape.fintypeObj
• CategoryTheory.Limits.WidePushoutShape.fintypeHom
• CategoryTheory.Limits.WidePushoutShape.fintypeObj
• CategoryTheory.Limits.fintypeWalkingPair
• CategoryTheory.Limits.fintypeWalkingParallelPair
• CategoryTheory.Limits.instFintypeWalkingParallelPairHom
• CategoryTheory.discreteFintype
• CategoryTheory.discreteHomFintype
• Fin.fintype
• Finset.Subtype.fintype
• Finset.fintypeCoeSort
• FinsetCoe.fintype
• Fintype.instEmpty
• Fintype.instPEmpty
• Fintype.subtypeEq
• Fintype.subtypeEq'
• Lex.fintype
• List.Subtype.fintype
• Multiplicative.fintype
• Multiset.Subtype.fintype
• OrderDual.fintype
• PLift.fintype
• PLift.fintypeProp
• PSigma.fintypePropLeft
• PSigma.fintypePropProp
• PSigma.fintypePropRight
• PUnit.fintype
• Prop.fintype
• Quotient.fintype
• Subtype.fintype
• ULift.fintype
• Unique.fintype
• Unit.fintype
• instFintypeOption
• pfunFintype

def Finset.univ {α : Type u_1} [Fintype α] : Finset α

univ is the universal finite set of type Finset α implied from the assumption Fintype α.

Equations

• Finset.univ = Fintype.elems

@[simp]

theorem Finset.mem_univ {α : Type u_1} [Fintype α] (x : α) : x ∈ Finset.univ

theorem Finset.mem_univ_val {α : Type u_1} [Fintype α] (x : α) : x ∈ Finset.univ.val

theorem Finset.eq_univ_iff_forall {α : Type u_1} [Fintype α] {s : Finset α} : s = Finset.univ ↔ ∀ (x : α), x ∈ s

theorem Finset.eq_univ_of_forall {α : Type u_1} [Fintype α] {s : Finset α} : (∀ (x : α), x ∈ s) → s = Finset.univ

@[simp]

theorem Finset.coe_univ {α : Type u_1} [Fintype α] : ↑Finset.univ = Set.univ

@[simp]

theorem Finset.coe_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} : ↑s = Set.univ ↔ s = Finset.univ

theorem Finset.Nonempty.eq_univ {α : Type u_1} [Fintype α] {s : Finset α} [Subsingleton α] : s.Nonempty → s = Finset.univ

theorem Finset.univ_nonempty_iff {α : Type u_1} [Fintype α] : Finset.univ.Nonempty ↔ Nonempty α

@[simp]

theorem Finset.univ_nonempty {α : Type u_1} [Fintype α] [Nonempty α] : Finset.univ.Nonempty

theorem Finset.univ_eq_empty_iff {α : Type u_1} [Fintype α] : Finset.univ = ∅ ↔ IsEmpty α

theorem Finset.univ_nontrivial_iff {α : Type u_1} [Fintype α] : Finset.univ.Nontrivial ↔ Nontrivial α

theorem Finset.univ_nontrivial {α : Type u_1} [Fintype α] [h : Nontrivial α] : Finset.univ.Nontrivial

@[simp]

theorem Finset.univ_eq_empty {α : Type u_1} [Fintype α] [IsEmpty α] : Finset.univ = ∅

@[simp]

theorem Finset.univ_unique {α : Type u_1} [Fintype α] [Unique α] : Finset.univ = {default}

@[simp]

theorem Finset.subset_univ {α : Type u_1} [Fintype α] (s : Finset α) : s ⊆ Finset.univ

instance Finset.boundedOrder {α : Type u_1} [Fintype α] : BoundedOrder (Finset α)

Equations

• Finset.boundedOrder = BoundedOrder.mk

@[simp]

theorem Finset.top_eq_univ {α : Type u_1} [Fintype α] : ⊤ = Finset.univ

theorem Finset.ssubset_univ_iff {α : Type u_1} [Fintype α] {s : Finset α} : s ⊂ Finset.univ ↔ s ≠ Finset.univ

@[simp]

theorem Finset.univ_subset_iff {α : Type u_1} [Fintype α] {s : Finset α} : Finset.univ ⊆ s ↔ s = Finset.univ

theorem Finset.codisjoint_left {α : Type u_1} [Fintype α] {s t : Finset α} : Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t

theorem Finset.codisjoint_right {α : Type u_1} [Fintype α] {s t : Finset α} : Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∈ s

instance Finset.booleanAlgebra {α : Type u_1} [Fintype α] [DecidableEq α] : BooleanAlgebra (Finset α)

Equations

• Finset.booleanAlgebra = GeneralizedBooleanAlgebra.toBooleanAlgebra

def Mathlib.Meta.elabFinsetBuilderSetOf : Lean.Elab.Term.TermElab

Elaborate set builder notation for Finset.

• {x | p x} is elaborated as Finset.filter (fun x ↦ p x) Finset.univ if the expected type is Finset ?α.
• {x : α | p x} is elaborated as Finset.filter (fun x : α ↦ p x) Finset.univ if the expected type is Finset ?α.
• {x ∉ s | p x} is elaborated as Finset.filter (fun x ↦ p x) sᶜ if either the expected type is Finset ?α or the expected type is not Set ?α and s has expected type Finset ?α.
• {x ≠ a | p x} is elaborated as Finset.filter (fun x ↦ p x) {a}ᶜ if the expected type is Finset ?α.

See also

• Data.Set.Defs for the Set builder notation elaborator that this elaborator partly overrides.
• Data.Finset.Basic for the Finset builder notation elaborator partly overriding this one for syntax of the form {x ∈ s | p x}.
• Data.Fintype.Basic for the Finset builder notation elaborator handling syntax of the form {x | p x}, {x : α | p x}, {x ∉ s | p x}, {x ≠ a | p x}.
• Order.LocallyFinite.Basic for the Finset builder notation elaborator handling syntax of the form {x ≤ a | p x}, {x ≥ a | p x}, {x < a | p x}, {x > a | p x}.

TODO: Write a delaborator

Equations

• One or more equations did not get rendered due to their size.

theorem Finset.sdiff_eq_inter_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s t : Finset α) : s \ t = s ∩ tᶜ

theorem Finset.compl_eq_univ_sdiff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : sᶜ = Finset.univ \ s

@[simp]

theorem Finset.mem_compl {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} : a ∈ sᶜ ↔ a ∉ s

theorem Finset.not_mem_compl {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} : a ∉ sᶜ ↔ a ∈ s

@[simp]

theorem Finset.coe_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : ↑sᶜ = (↑s)ᶜ

@[simp]

theorem Finset.compl_subset_compl {α : Type u_1} [Fintype α] {s t : Finset α} [DecidableEq α] : sᶜ ⊆ tᶜ ↔ t ⊆ s

@[simp]

theorem Finset.compl_ssubset_compl {α : Type u_1} [Fintype α] {s t : Finset α} [DecidableEq α] : sᶜ ⊂ tᶜ ↔ t ⊂ s

theorem Finset.subset_compl_comm {α : Type u_1} [Fintype α] {s t : Finset α} [DecidableEq α] : s ⊆ tᶜ ↔ t ⊆ sᶜ

@[simp]

theorem Finset.subset_compl_singleton {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} : s ⊆ {a}ᶜ ↔ a ∉ s

@[simp]

theorem Finset.compl_empty {α : Type u_1} [Fintype α] [DecidableEq α] : ∅ᶜ = Finset.univ

@[simp]

theorem Finset.compl_univ {α : Type u_1} [Fintype α] [DecidableEq α] : Finset.univᶜ = ∅

@[simp]

theorem Finset.compl_eq_empty_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : sᶜ = ∅ ↔ s = Finset.univ

@[simp]

theorem Finset.compl_eq_univ_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : sᶜ = Finset.univ ↔ s = ∅

@[simp]

theorem Finset.union_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : s ∪ sᶜ = Finset.univ

@[simp]

theorem Finset.inter_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : s ∩ sᶜ = ∅

@[simp]

theorem Finset.compl_union {α : Type u_1} [Fintype α] [DecidableEq α] (s t : Finset α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ

@[simp]

theorem Finset.compl_inter {α : Type u_1} [Fintype α] [DecidableEq α] (s t : Finset α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ

@[simp]

theorem Finset.compl_erase {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} : (s.erase a)ᶜ = insert a sᶜ

@[simp]

theorem Finset.compl_insert {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} : (insert a s)ᶜ = sᶜ.erase a

theorem Finset.insert_compl_insert {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} (ha : a ∉ s) : insert a (insert a s)ᶜ = sᶜ

@[simp]

theorem Finset.insert_compl_self {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) : insert x {x}ᶜ = Finset.univ

@[simp]

theorem Finset.compl_filter {α : Type u_1} [Fintype α] [DecidableEq α] (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] : (Finset.filter p Finset.univ)ᶜ = Finset.filter (fun (x : α) => ¬p x) Finset.univ

theorem Finset.compl_ne_univ_iff_nonempty {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : sᶜ ≠ Finset.univ ↔ s.Nonempty

theorem Finset.compl_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (a : α) : {a}ᶜ = Finset.univ.erase a

theorem Finset.insert_inj_on' {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : Set.InjOn (fun (a : α) => insert a s) ↑sᶜ

theorem Finset.image_univ_of_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] {f : β → α} (hf : Function.Surjective f) : Finset.image f Finset.univ = Finset.univ

@[simp]

theorem Finset.image_univ_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] (f : β ≃ α) : Finset.image (⇑f) Finset.univ = Finset.univ

@[simp]

theorem Finset.univ_inter {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : Finset.univ ∩ s = s

@[simp]

theorem Finset.inter_univ {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : s ∩ Finset.univ = s

@[simp]

theorem Finset.inter_eq_univ {α : Type u_1} [Fintype α] {s t : Finset α} [DecidableEq α] : s ∩ t = Finset.univ ↔ s = Finset.univ ∧ t = Finset.univ

theorem Finset.singleton_eq_univ {α : Type u_1} [Fintype α] [Subsingleton α] (a : α) : {a} = Finset.univ

theorem Finset.map_univ_of_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : β ↪ α} (hf : Function.Surjective ⇑f) : Finset.map f Finset.univ = Finset.univ

@[simp]

theorem Finset.map_univ_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : β ≃ α) : Finset.map f.toEmbedding Finset.univ = Finset.univ

theorem Finset.univ_map_equiv_to_embedding {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (e : α ≃ β) : Finset.map e.toEmbedding Finset.univ = Finset.univ

@[simp]

theorem Finset.univ_filter_exists {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) [Fintype β] [DecidablePred fun (y : β) => ∃ (x : α), f x = y] [DecidableEq β] : Finset.filter (fun (y : β) => ∃ (x : α), f x = y) Finset.univ = Finset.image f Finset.univ

theorem Finset.univ_filter_mem_range {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) [Fintype β] [DecidablePred fun (y : β) => y ∈ Set.range f] [DecidableEq β] : Finset.filter (fun (y : β) => y ∈ Set.range f) Finset.univ = Finset.image f Finset.univ

Note this is a special case of (Finset.image_preimage f univ _).symm.

theorem Finset.coe_filter_univ {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] : ↑(Finset.filter p Finset.univ) = {x : α | p x}

@[simp]

theorem Finset.subtype_eq_univ {α : Type u_1} {s : Finset α} {p : α → Prop} [DecidablePred p] [Fintype { a : α // p a }] : Finset.subtype p s = Finset.univ ↔ ∀ ⦃a : α⦄, p a → a ∈ s

@[simp]

theorem Finset.subtype_univ {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a : α // p a }] : Finset.subtype p Finset.univ = Finset.univ

theorem Finset.univ_map_subtype {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a : α // p a }] : Finset.map (Function.Embedding.subtype p) Finset.univ = Finset.filter p Finset.univ

theorem Finset.univ_val_map_subtype_val {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a : α // p a }] : Multiset.map Subtype.val Finset.univ.val = (Finset.filter p Finset.univ).val

theorem Finset.univ_val_map_subtype_restrict {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) (p : α → Prop) [DecidablePred p] [Fintype { a : α // p a }] : Multiset.map (Subtype.restrict p f) Finset.univ.val = Multiset.map f (Finset.filter p Finset.univ).val

instance Fintype.decidablePiFintype {α : Type u_5} {β : α → Type u_4} [(a : α) → DecidableEq (β a)] [Fintype α] : DecidableEq ((a : α) → β a)

Equations

• Fintype.decidablePiFintype f g = decidable_of_iff (∀ a ∈ Fintype.elems, f a = g a) ⋯

instance Fintype.decidableForallFintype {α : Type u_1} {p : α → Prop} [DecidablePred p] [Fintype α] : Decidable (∀ (a : α), p a)

Equations

• Fintype.decidableForallFintype = decidable_of_iff (∀ a ∈ Finset.univ, p a) ⋯

instance Fintype.decidableExistsFintype {α : Type u_1} {p : α → Prop} [DecidablePred p] [Fintype α] : Decidable (∃ (a : α), p a)

Equations

• Fintype.decidableExistsFintype = decidable_of_iff (∃ a ∈ Finset.univ, p a) ⋯

instance Fintype.decidableMemRangeFintype {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α → β) : DecidablePred fun (x : β) => x ∈ Set.range f

Equations

• Fintype.decidableMemRangeFintype f x = Fintype.decidableExistsFintype

instance Fintype.decidableSubsingleton {α : Type u_1} [Fintype α] [DecidableEq α] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] : Decidable s.Subsingleton

Equations

• Fintype.decidableSubsingleton = decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, a = b) ⋯

instance Fintype.decidableEqEquivFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] : DecidableEq (α ≃ β)

Equations

• Fintype.decidableEqEquivFintype a b = decidable_of_iff (a.toFun = b.toFun) ⋯

instance Fintype.decidableEqEmbeddingFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] : DecidableEq (α ↪ β)

Equations

• Fintype.decidableEqEmbeddingFintype a b = decidable_of_iff (⇑a = ⇑b) ⋯

instance Fintype.decidableInjectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] : DecidablePred Function.Injective

Equations

• Fintype.decidableInjectiveFintype x = id inferInstance

instance Fintype.decidableSurjectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Fintype β] : DecidablePred Function.Surjective

Equations

• Fintype.decidableSurjectiveFintype x = id inferInstance

instance Fintype.decidableBijectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] : DecidablePred Function.Bijective

Equations

• Fintype.decidableBijectiveFintype x = id inferInstance

instance Fintype.decidableRightInverseFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] (f : α → β) (g : β → α) : Decidable (Function.RightInverse f g)

Equations

• Fintype.decidableRightInverseFintype f g = inferInstance

instance Fintype.decidableLeftInverseFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype β] (f : α → β) (g : β → α) : Decidable (Function.LeftInverse f g)

Equations

• Fintype.decidableLeftInverseFintype f g = inferInstance

def Fintype.ofMultiset {α : Type u_1} [DecidableEq α] (s : Multiset α) (H : ∀ (x : α), x ∈ s) : Fintype α

Construct a proof of Fintype α from a universal multiset

Equations

• Fintype.ofMultiset s H = { elems := s.toFinset, complete := ⋯ }

def Fintype.ofList {α : Type u_1} [DecidableEq α] (l : List α) (H : ∀ (x : α), x ∈ l) : Fintype α

Construct a proof of Fintype α from a universal list

Equations

• Fintype.ofList l H = { elems := l.toFinset, complete := ⋯ }

instance Fintype.subsingleton (α : Type u_4) : Subsingleton (Fintype α)

Equations

• ⋯ = ⋯

instance Fintype.instFastSubsingleton (α : Type u_4) : Lean.Meta.FastSubsingleton (Fintype α)

Equations

• ⋯ = ⋯

def Fintype.subtype {α : Type u_1} {p : α → Prop} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ p x) : Fintype { x : α // p x }

Given a predicate that can be represented by a finset, the subtype associated to the predicate is a fintype.

Equations

• Fintype.subtype s H = { elems := { val := Multiset.pmap Subtype.mk s.val ⋯, nodup := ⋯ }, complete := ⋯ }

def Fintype.ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) : Fintype ↑p

Construct a fintype from a finset with the same elements.

Equations

• Fintype.ofFinset s H = Fintype.subtype s H

def Fintype.ofBijective {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) (H : Function.Bijective f) : Fintype β

If f : α → β is a bijection and α is a fintype, then β is also a fintype.

Equations

• Fintype.ofBijective f H = { elems := Finset.map { toFun := f, inj' := ⋯ } Finset.univ, complete := ⋯ }

def Fintype.ofSurjective {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] (f : α → β) (H : Function.Surjective f) : Fintype β

If f : α → β is a surjection and α is a fintype, then β is also a fintype.

Equations

• Fintype.ofSurjective f H = { elems := Finset.image f Finset.univ, complete := ⋯ }

@[simp]

theorem Finset.filter_univ_mem {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : Finset.filter (fun (x : α) => x ∈ s) Finset.univ = s

instance Finset.decidableCodisjoint {α : Type u_1} [Fintype α] [DecidableEq α] {s t : Finset α} : Decidable (Codisjoint s t)

Equations

• Finset.decidableCodisjoint = decidable_of_iff (∀ ⦃a : α⦄, a ∉ s → a ∈ t) ⋯

instance Finset.decidableIsCompl {α : Type u_1} [Fintype α] [DecidableEq α] {s t : Finset α} : Decidable (IsCompl s t)

Equations

• Finset.decidableIsCompl = decidable_of_iff' (Disjoint s t ∧ Codisjoint s t) ⋯

def Function.Injective.invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) : ↑(Set.range f) → α

The inverse of an hf : injective function f : α → β, of the type ↥(Set.range f) → α. This is the computable version of Function.invFun that requires Fintype α and DecidableEq β, or the function version of applying (Equiv.ofInjective f hf).symm. This function should not usually be used for actual computation because for most cases, an explicit inverse can be stated that has better computational properties. This function computes by checking all terms a : α to find the f a = b, so it is O(N) where N = Fintype.card α.

Equations

• hf.invOfMemRange b = Finset.choose (fun (a : α) => f a = ↑b) Finset.univ ⋯

theorem Function.Injective.left_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (b : ↑(Set.range f)) : f (hf.invOfMemRange b) = ↑b

@[simp]

theorem Function.Injective.right_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (a : α) : hf.invOfMemRange ⟨f a, ⋯⟩ = a

theorem Function.Injective.invFun_restrict {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) [Nonempty α] : (Set.range f).restrict (Function.invFun f) = hf.invOfMemRange

theorem Function.Injective.invOfMemRange_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) : Function.Surjective hf.invOfMemRange

def Function.Embedding.invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) (b : ↑(Set.range ⇑f)) : α

The inverse of an embedding f : α ↪ β, of the type ↥(Set.range f) → α. This is the computable version of Function.invFun that requires Fintype α and DecidableEq β, or the function version of applying (Equiv.ofInjective f f.injective).symm. This function should not usually be used for actual computation because for most cases, an explicit inverse can be stated that has better computational properties. This function computes by checking all terms a : α to find the f a = b, so it is O(N) where N = Fintype.card α.

Equations

• f.invOfMemRange b = ⋯.invOfMemRange b

@[simp]

theorem Function.Embedding.left_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) (b : ↑(Set.range ⇑f)) : f (f.invOfMemRange b) = ↑b

@[simp]

theorem Function.Embedding.right_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) (a : α) : f.invOfMemRange ⟨f a, ⋯⟩ = a

theorem Function.Embedding.invFun_restrict {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) [Nonempty α] : (Set.range ⇑f).restrict (Function.invFun ⇑f) = f.invOfMemRange

theorem Function.Embedding.invOfMemRange_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) : Function.Surjective f.invOfMemRange

noncomputable def Fintype.ofInjective {α : Type u_1} {β : Type u_2} [Fintype β] (f : α → β) (H : Function.Injective f) : Fintype α

Given an injective function to a fintype, the domain is also a fintype. This is noncomputable because injectivity alone cannot be used to construct preimages.

Equations

• Fintype.ofInjective f H = if hα : Nonempty α then Fintype.ofSurjective (Function.invFun f) ⋯ else { elems := ∅, complete := ⋯ }

def Fintype.ofEquiv {β : Type u_2} (α : Type u_4) [Fintype α] (f : α ≃ β) : Fintype β

If f : α ≃ β and α is a fintype, then β is also a fintype.

Equations

• Fintype.ofEquiv α f = Fintype.ofBijective ⇑f ⋯

def Fintype.ofSubsingleton {α : Type u_1} (a : α) [Subsingleton α] : Fintype α

Any subsingleton type with a witness is a fintype (with one term).

Equations

• Fintype.ofSubsingleton a = { elems := {a}, complete := ⋯ }

theorem Fintype.univ_ofSubsingleton {α : Type u_1} (a : α) [Subsingleton α] : Finset.univ = {a}

def Fintype.ofIsEmpty {α : Type u_1} [IsEmpty α] : Fintype α

An empty type is a fintype. Not registered as an instance, to make sure that there aren't two conflicting Fintype ι instances around when casing over whether a fintype ι is empty or not.

Equations

• Fintype.ofIsEmpty = { elems := ∅, complete := ⋯ }

theorem Fintype.univ_ofIsEmpty {α : Type u_1} [IsEmpty α] : Finset.univ = ∅

Note: this lemma is specifically about Fintype.ofIsEmpty. For a statement about arbitrary Fintype instances, use Finset.univ_eq_empty.

instance Fintype.instEmpty : Fintype Empty

Equations

• Fintype.instEmpty = Fintype.ofIsEmpty

instance Fintype.instPEmpty : Fintype PEmpty.{u_4 + 1}

Equations

• Fintype.instPEmpty = Fintype.ofIsEmpty

def Set.toFinset {α : Type u_1} (s : Set α) [Fintype ↑s] : Finset α

Construct a finset enumerating a set s, given a Fintype instance.

Equations

• s.toFinset = Finset.map (Function.Embedding.subtype fun (x : α) => x ∈ s) Finset.univ

theorem Set.toFinset_congr {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] (h : s = t) : s.toFinset = t.toFinset

@[simp]

theorem Set.mem_toFinset {α : Type u_1} {s : Set α} [Fintype ↑s] {a : α} : a ∈ s.toFinset ↔ a ∈ s

theorem Set.toFinset_ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) : p.toFinset = s

Many Fintype instances for sets are defined using an extensionally equal Finset. Rewriting s.toFinset with Set.toFinset_ofFinset replaces the term with such a Finset.

def Set.decidableMemOfFintype {α : Type u_1} [DecidableEq α] (s : Set α) [Fintype ↑s] (a : α) : Decidable (a ∈ s)

Membership of a set with a Fintype instance is decidable.

Using this as an instance leads to potential loops with Subtype.fintype under certain decidability assumptions, so it should only be declared a local instance.

Equations

• s.decidableMemOfFintype a = decidable_of_iff (a ∈ s.toFinset) ⋯

@[simp]

theorem Set.coe_toFinset {α : Type u_1} (s : Set α) [Fintype ↑s] : ↑s.toFinset = s

@[simp]

theorem Set.toFinset_nonempty {α : Type u_1} {s : Set α} [Fintype ↑s] : s.toFinset.Nonempty ↔ s.Nonempty

theorem Set.Aesop.toFinset_nonempty_of_nonempty {α : Type u_1} {s : Set α} [Fintype ↑s] : s.Nonempty → s.toFinset.Nonempty

Alias of the reverse direction of Set.toFinset_nonempty.

@[simp]

theorem Set.toFinset_inj {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] : s.toFinset = t.toFinset ↔ s = t

theorem Set.toFinset_subset_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] : s.toFinset ⊆ t.toFinset ↔ s ⊆ t

@[simp]

theorem Set.toFinset_ssubset {α : Type u_1} {s : Set α} [Fintype ↑s] {t : Finset α} : s.toFinset ⊂ t ↔ s ⊂ ↑t

@[simp]

theorem Set.subset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype ↑t] : s ⊆ t.toFinset ↔ ↑s ⊆ t

@[simp]

theorem Set.ssubset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype ↑t] : s ⊂ t.toFinset ↔ ↑s ⊂ t

theorem Set.toFinset_ssubset_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] : s.toFinset ⊂ t.toFinset ↔ s ⊂ t

@[simp]

theorem Set.toFinset_subset {α : Type u_1} {s : Set α} [Fintype ↑s] {t : Finset α} : s.toFinset ⊆ t ↔ s ⊆ ↑t

theorem Set.toFinset_mono {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] : s ⊆ t → s.toFinset ⊆ t.toFinset

Alias of the reverse direction of Set.toFinset_subset_toFinset.

theorem Set.toFinset_strict_mono {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] : s ⊂ t → s.toFinset ⊂ t.toFinset

Alias of the reverse direction of Set.toFinset_ssubset_toFinset.

@[simp]

theorem Set.disjoint_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] : Disjoint s.toFinset t.toFinset ↔ Disjoint s t

@[simp]

theorem Set.toFinset_inter {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s ∩ t)] : (s ∩ t).toFinset = s.toFinset ∩ t.toFinset

@[simp]

theorem Set.toFinset_union {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s ∪ t)] : (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

@[simp]

theorem Set.toFinset_diff {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s \ t)] : (s \ t).toFinset = s.toFinset \ t.toFinset

@[simp]

theorem Set.toFinset_symmDiff {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(symmDiff s t)] : (symmDiff s t).toFinset = symmDiff s.toFinset t.toFinset

@[simp]

theorem Set.toFinset_compl {α : Type u_1} (s : Set α) [DecidableEq α] [Fintype ↑s] [Fintype α] [Fintype ↑sᶜ] : sᶜ.toFinset = s.toFinsetᶜ

@[simp]

theorem Set.toFinset_empty {α : Type u_1} [Fintype ↑∅] : ∅.toFinset = ∅

@[simp]

theorem Set.toFinset_univ {α : Type u_1} [Fintype α] [Fintype ↑Set.univ] : Set.univ.toFinset = Finset.univ

@[simp]

theorem Set.toFinset_eq_empty {α : Type u_1} {s : Set α} [Fintype ↑s] : s.toFinset = ∅ ↔ s = ∅

@[simp]

theorem Set.toFinset_eq_univ {α : Type u_1} {s : Set α} [Fintype α] [Fintype ↑s] : s.toFinset = Finset.univ ↔ s = Set.univ

@[simp]

theorem Set.toFinset_setOf {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype ↑{x : α | p x}] : {x : α | p x}.toFinset = Finset.filter p Finset.univ

theorem Set.toFinset_ssubset_univ {α : Type u_1} [Fintype α] {s : Set α} [Fintype ↑s] : s.toFinset ⊂ Finset.univ ↔ s ⊂ Set.univ

@[simp]

theorem Set.toFinset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Set α) [Fintype ↑s] [Fintype ↑(f '' s)] : (f '' s).toFinset = Finset.image f s.toFinset

@[simp]

theorem Set.toFinset_range {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] (f : β → α) [Fintype ↑(Set.range f)] : (Set.range f).toFinset = Finset.image f Finset.univ

@[simp]

theorem Set.toFinset_singleton {α : Type u_1} (a : α) [Fintype ↑{a}] : {a}.toFinset = {a}

@[simp]

theorem Set.toFinset_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Set α} [Fintype ↑(insert a s)] [Fintype ↑s] : (insert a s).toFinset = insert a s.toFinset

theorem Set.filter_mem_univ_eq_toFinset {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] [DecidablePred fun (x : α) => x ∈ s] : Finset.filter (fun (x : α) => x ∈ s) Finset.univ = s.toFinset

@[simp]

theorem Finset.toFinset_coe {α : Type u_1} (s : Finset α) [Fintype ↑↑s] : (↑s).toFinset = s

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

Equations

• Fin.fintype n = { elems := { val := ↑(List.finRange n), nodup := ⋯ }, complete := ⋯ }

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

@[simp]

theorem List.toFinset_finRange (n : ℕ) : (List.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 Fin.succ Finset.univ = {0}ᶜ

@[simp]

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

theorem Fin.univ_succ (n : ℕ) : Finset.univ = Finset.cons 0 (Finset.map { toFun := Fin.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 (Fin.last n) (Finset.map Fin.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 α

Equations

• Unique.fintype = Fintype.ofSubsingleton default

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.

Equations

• Fintype.subtypeEq y = Fintype.subtype {y} ⋯

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.

Equations

• Fintype.subtypeEq' y = Fintype.subtype {y} ⋯

theorem Fintype.univ_empty : Finset.univ = ∅

theorem Fintype.univ_pempty : Finset.univ = ∅

instance Unit.fintype : Fintype Unit

Equations

• Unit.fintype = Fintype.ofSubsingleton ()

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

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

Equations

• PUnit.fintype = Fintype.ofSubsingleton PUnit.unit

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

instance Bool.fintype : Fintype Bool

Equations

• Bool.fintype = { elems := { val := {true, false}, nodup := Bool.fintype.proof_1 }, complete := Bool.fintype.proof_2 }

@[simp]

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

instance Additive.fintype {α : Type u_1} [Fintype α] : Fintype (Additive α)

Equations

• Additive.fintype = Fintype.ofEquiv α Additive.ofMul

instance Multiplicative.fintype {α : Type u_1} [Fintype α] : Fintype (Multiplicative α)

Equations

• Multiplicative.fintype = Fintype.ofEquiv α Multiplicative.ofAdd

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

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

Equations

• Fintype.prodLeft = { elems := Finset.image Prod.fst Finset.univ, complete := ⋯ }

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

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

Equations

• Fintype.prodRight = { elems := Finset.image Prod.snd Finset.univ, complete := ⋯ }

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

Equations

• ULift.fintype α = Fintype.ofEquiv α Equiv.ulift.symm

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

Equations

• PLift.fintype α = Fintype.ofEquiv α Equiv.plift.symm

instance OrderDual.fintype (α : Type u_4) [Fintype α] : Fintype αᵒᵈ

Equations

• OrderDual.fintype α = inst

instance OrderDual.finite (α : Type u_4) [Finite α] : Finite αᵒᵈ

Equations

• ⋯ = inst

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

Equations

• Lex.fintype α = inst

Fintype (s : Finset α)

instance Finset.fintypeCoeSort {α : Type u} (s : Finset α) : Fintype { x : α // x ∈ s }

Equations

• s.fintypeCoeSort = { elems := s.attach, complete := ⋯ }

@[simp]

theorem Finset.univ_eq_attach {α : Type u} (s : Finset α) : Finset.univ = s.attach

theorem Fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} : ↑(Finset.image f Finset.univ) = Set.range f

instance List.Subtype.fintype {α : Type u_1} [DecidableEq α] (l : List α) : Fintype { x : α // x ∈ l }

Equations

• List.Subtype.fintype l = Fintype.ofList l.attach ⋯

instance Multiset.Subtype.fintype {α : Type u_1} [DecidableEq α] (s : Multiset α) : Fintype { x : α // x ∈ s }

Equations

• Multiset.Subtype.fintype s = Fintype.ofMultiset s.attach ⋯

instance Finset.Subtype.fintype {α : Type u_1} (s : Finset α) : Fintype { x : α // x ∈ s }

Equations

• Finset.Subtype.fintype s = { elems := s.attach, complete := ⋯ }

instance FinsetCoe.fintype {α : Type u_1} (s : Finset α) : Fintype ↑↑s

Equations

• FinsetCoe.fintype s = Finset.Subtype.fintype s

theorem Finset.attach_eq_univ {α : Type u_1} {s : Finset α} : s.attach = Finset.univ

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

Equations

• PLift.fintypeProp p = { elems := if h : p then {{ down := h }} else ∅, complete := ⋯ }

instance Prop.fintype : Fintype Prop

Equations

• «Prop».fintype = { elems := { val := {True, False}, nodup := «Prop».fintype.proof_1 }, complete := «Prop».fintype.proof_2 }

@[simp]

theorem Fintype.univ_Prop : Finset.univ = {True, False}

instance Subtype.fintype {α : Type u_1} (p : α → Prop) [DecidablePred p] [Fintype α] : Fintype { x : α // p x }

Equations

• Subtype.fintype p = Fintype.subtype (Finset.filter p Finset.univ) ⋯

def setFintype {α : Type u_1} [Fintype α] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : Fintype ↑s

A set on a fintype, when coerced to a type, is a fintype.

Equations

• setFintype s = Subtype.fintype fun (x : α) => x ∈ s

noncomputable def Fintype.finsetEquivSet {α : Type u_1} [Fintype α] : Finset α ≃ Set α

Given Fintype α, finsetEquivSet is the equiv between Finset α and Set α. (All sets on a finite type are finite.)

Equations

• Fintype.finsetEquivSet = { toFun := Finset.toSet, invFun := fun (s : Set α) => s.toFinset, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Fintype.coe_finsetEquivSet {α : Type u_1} [Fintype α] : ⇑Fintype.finsetEquivSet = Finset.toSet

@[simp]

theorem Fintype.finsetEquivSet_apply {α : Type u_1} [Fintype α] (s : Finset α) : Fintype.finsetEquivSet s = ↑s

@[simp]

theorem Fintype.finsetEquivSet_symm_apply {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] : Fintype.finsetEquivSet.symm s = s.toFinset

noncomputable def Fintype.finsetOrderIsoSet {α : Type u_1} [Fintype α] : Finset α ≃o Set α

Given a fintype α, finsetOrderIsoSet is the order isomorphism between Finset α and Set α (all sets on a finite type are finite).

Equations

• Fintype.finsetOrderIsoSet = { toEquiv := Fintype.finsetEquivSet, map_rel_iff' := ⋯ }

@[simp]

theorem Fintype.finsetOrderIsoSet_toEquiv {α : Type u_1} [Fintype α] : Fintype.finsetOrderIsoSet.toEquiv = Fintype.finsetEquivSet

@[simp]

theorem Fintype.coe_finsetOrderIsoSet {α : Type u_1} [Fintype α] : ⇑Fintype.finsetOrderIsoSet = Finset.toSet

@[simp]

theorem Fintype.coe_finsetOrderIsoSet_symm {α : Type u_1} [Fintype α] : ⇑Fintype.finsetOrderIsoSet.symm = ⇑Fintype.finsetEquivSet.symm

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

Equations

• Quotient.fintype s = Fintype.ofSurjective Quotient.mk'' ⋯

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

Equations

• PSigma.fintypePropLeft = if h : α then Fintype.ofEquiv (β h) { toFun := fun (x : β h) => ⟨h, x⟩, invFun := PSigma.snd, left_inv := ⋯, right_inv := ⋯ } else { elems := ∅, complete := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• PSigma.fintypePropProp = if h : ∃ (a : α), β a then { elems := {⟨⋯, ⋯⟩}, complete := ⋯ } else { elems := ∅, complete := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

theorem mem_image_univ_iff_mem_range {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq β] {f : α → β} {b : β} : b ∈ Finset.image f Finset.univ ↔ b ∈ Set.range f

def Fintype.chooseX {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (hp : ∃! a : α, p a) : { a : α // p a }

Given a fintype α and a predicate p, associate to a proof that there is a unique element of α satisfying p this unique element, as an element of the corresponding subtype.

Equations

• Fintype.chooseX p hp = ⟨Finset.choose p Finset.univ ⋯, ⋯⟩

def Fintype.choose {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (hp : ∃! a : α, p a) : α

Given a fintype α and a predicate p, associate to a proof that there is a unique element of α satisfying p this unique element, as an element of α.

Equations

• Fintype.choose p hp = ↑(Fintype.chooseX p hp)

theorem Fintype.choose_spec {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (hp : ∃! a : α, p a) : p (Fintype.choose p hp)

theorem Fintype.choose_subtype_eq {α : Type u_4} (p : α → Prop) [Fintype { a : α // p a }] [DecidableEq α] (x : { a : α // p a }) (h : ∃! a : { a : α // p a }, ↑a = ↑x := ⋯) : Fintype.choose (fun (y : { a : α // p a }) => ↑y = ↑x) h = x

def Fintype.bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (f_bij : Function.Bijective f) (b : β) : α

bijInv f is the unique inverse to a bijection f. This acts as a computable alternative to Function.invFun.

Equations

• Fintype.bijInv f_bij b = Fintype.choose (fun (a : α) => f a = b) ⋯

theorem Fintype.leftInverse_bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (f_bij : Function.Bijective f) : Function.LeftInverse (Fintype.bijInv f_bij) f

theorem Fintype.rightInverse_bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (f_bij : Function.Bijective f) : Function.RightInverse (Fintype.bijInv f_bij) f

theorem Fintype.bijective_bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (f_bij : Function.Bijective f) : Function.Bijective (Fintype.bijInv f_bij)

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

Equations

• One or more equations did not get rendered due to their size.

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

A Nonempty Fintype constructively contains an element.

Equations

• truncOfNonemptyFintype α = truncOfMultisetExistsMem Finset.univ.val ⋯

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.

Equations

• truncSigmaOfExists h = truncOfNonemptyFintype ((a : α) ×' P a)

@[simp]

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

@[simp]

theorem Multiset.map_univ_val_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α ≃ β) : Multiset.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 ↔ Multiset.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.

Equations

• seqOfForallFinsetExistsAux P r h x = Classical.choose ⋯

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 fun (m n : ℕ) => r (f m) (f n)

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.

def finsetStx : Lean.ParserDescr

finset% t elaborates t as a Finset. If t is a Set, then inserts Set.toFinset. Does not make use of the expected type; useful for big operators over finsets.

#check finset% Finset.range 2 -- Finset Nat
#check finset% (Set.univ : Set Bool) -- Finset Bool

Equations

• finsetStx = Lean.ParserDescr.node `finsetStx 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "finset% ") (Lean.ParserDescr.cat `term 0))

def precheckFinsetStx : Lean.Elab.Term.Quotation.Precheck

quot_precheck for the finset% syntax.

Equations

• One or more equations did not get rendered due to their size.