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.

ink

class Fintype (α : Type u_1) : Type u_1

• The Finset containing all elements of a Fintype

  elems : Finset α

• A proof that elems contains every element of the type

  complete : ∀ (x : α), x ∈ elems

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.

ink

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

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

Equations

• Finset.univ = Fintype.elems

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• Finset.boundedOrder = let src := inferInstanceAs (OrderBot (Finset α)); BoundedOrder.mk

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

Equations

• Finset.booleanAlgebra = GeneralizedBooleanAlgebra.toBooleanAlgebra

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem Finset.piecewise_univ {α : Type u_1} [inst : Fintype α] [inst : (i : α) → Decidable (i ∈ Finset.univ)] {δ : α → Sort u_2} (f : (i : α) → δ i) (g : (i : α) → δ i) : Finset.piecewise Finset.univ f g = f

ink

theorem Finset.piecewise_compl {α : Type u_1} [inst : Fintype α] [inst : DecidableEq α] (s : Finset α) [inst : (i : α) → Decidable (i ∈ s)] [inst : (i : α) → Decidable (i ∈ sᶜ)] {δ : α → Sort u_2} (f : (i : α) → δ i) (g : (i : α) → δ i) : Finset.piecewise (sᶜ) f g = Finset.piecewise s g f

ink

@[simp]

theorem Finset.piecewise_erase_univ {α : Type u_2} [inst : Fintype α] {δ : α → Sort u_1} [inst : DecidableEq α] (a : α) (f : (a : α) → δ a) (g : (a : α) → δ a) : Finset.piecewise (Finset.erase Finset.univ a) f g = Function.update f a (g a)

ink

theorem Finset.univ_map_equiv_to_embedding {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (e : α ≃ β) : Finset.map (Equiv.toEmbedding e) Finset.univ = Finset.univ

ink

@[simp]

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

ink

theorem Finset.univ_filter_mem_range {α : Type u_2} {β : Type u_1} [inst : Fintype α] (f : α → β) [inst : Fintype β] [inst : DecidablePred fun y => y ∈ Set.range f] [inst : 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.

ink

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

ink

instance Fintype.decidablePiFintype {α : Type u_1} {β : α → Type u_2} [inst : (a : α) → DecidableEq (β a)] [inst : Fintype α] : DecidableEq ((a : α) → β a)

Equations

• Fintype.decidablePiFintype f g = decidable_of_iff (∀ (a : α), a ∈ Fintype.elems → f a = g a) (_ : (∀ (a : α), a ∈ Fintype.elems → f a = g a) ↔ f = g)

ink

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

Equations

• Fintype.decidableForallFintype = decidable_of_iff ((a : α) → a ∈ Finset.univ → p a) (_ : ((a : α) → a ∈ Finset.univ → p a) ↔ (a : α) → p a)

ink

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

Equations

• Fintype.decidableExistsFintype = decidable_of_iff (∃ a, a ∈ Finset.univ ∧ p a) (_ : (∃ x, x ∈ Finset.univ ∧ p x) ↔ ∃ a, p a)

ink

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

Equations

• Fintype.decidableMemRangeFintype f x = Fintype.decidableExistsFintype

ink

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

Equations

• Fintype.decidableEqEquivFintype a b = decidable_of_iff (a.toFun = b.toFun) (_ : ↑a = ↑b ↔ a = b)

ink

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

Equations

• Fintype.decidableEqEmbeddingFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)

ink

def Fintype.decidableEqZeroHomFintype.proof_1 {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Zero β] (a : ZeroHom α β) (b : ZeroHom α β) : ↑a = ↑b ↔ a = b

Equations

• (_ : ↑a = ↑b ↔ a = b) = (_ : ↑a = ↑b ↔ a = b)

ink

instance Fintype.decidableEqZeroHomFintype {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst : Fintype α] [inst : Zero α] [inst : Zero β] : DecidableEq (ZeroHom α β)

Equations

• Fintype.decidableEqZeroHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)

ink

instance Fintype.decidableEqOneHomFintype {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst : Fintype α] [inst : One α] [inst : One β] : DecidableEq (OneHom α β)

Equations

• Fintype.decidableEqOneHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)

ink

instance Fintype.decidableEqAddHomFintype {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst : Fintype α] [inst : Add α] [inst : Add β] : DecidableEq (AddHom α β)

Equations

• Fintype.decidableEqAddHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)

ink

def Fintype.decidableEqAddHomFintype.proof_1 {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Add β] (a : AddHom α β) (b : AddHom α β) : ↑a = ↑b ↔ a = b

Equations

• (_ : ↑a = ↑b ↔ a = b) = (_ : ↑a = ↑b ↔ a = b)

ink

instance Fintype.decidableEqMulHomFintype {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst : Fintype α] [inst : Mul α] [inst : Mul β] : DecidableEq (α →ₙ* β)

Equations

• Fintype.decidableEqMulHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)

ink

def Fintype.decidableEqAddMonoidHomFintype.proof_1 {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst : AddZeroClass β] (a : α →+ β) (b : α →+ β) : ↑a = ↑b ↔ a = b

Equations

• (_ : ↑a = ↑b ↔ a = b) = (_ : ↑a = ↑b ↔ a = b)

ink

instance Fintype.decidableEqAddMonoidHomFintype {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst : Fintype α] [inst : AddZeroClass α] [inst : AddZeroClass β] : DecidableEq (α →+ β)

Equations

• Fintype.decidableEqAddMonoidHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)

ink

instance Fintype.decidableEqMonoidHomFintype {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst : Fintype α] [inst : MulOneClass α] [inst : MulOneClass β] : DecidableEq (α →* β)

Equations

• Fintype.decidableEqMonoidHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)

ink

instance Fintype.decidableEqMonoidWithZeroHomFintype {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst : Fintype α] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] : DecidableEq (α →*₀ β)

Equations

• Fintype.decidableEqMonoidWithZeroHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)

ink

instance Fintype.decidableEqRingHomFintype {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst : Fintype α] [inst : Semiring α] [inst : Semiring β] : DecidableEq (α →+* β)

Equations

• Fintype.decidableEqRingHomFintype a b = decidable_of_iff (↑a = ↑b) (_ : ↑a = ↑b ↔ a = b)

ink

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

Equations

• Fintype.decidableInjectiveFintype x = id inferInstance

ink

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

Equations

• Fintype.decidableSurjectiveFintype x = id inferInstance

ink

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

Equations

• Fintype.decidableBijectiveFintype x = id inferInstance

ink

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

Equations

• Fintype.decidableRightInverseFintype f g = let_fun this := inferInstance; this

ink

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

Equations

• Fintype.decidableLeftInverseFintype f g = let_fun this := inferInstance; this

ink

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

Construct a proof of Fintype α from a universal multiset

Equations

• Fintype.ofMultiset s H = { elems := Multiset.toFinset s, complete := (_ : ∀ (x : α), x ∈ Multiset.toFinset s) }

ink

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

Construct a proof of Fintype α from a universal list

Equations

• Fintype.ofList l H = { elems := List.toFinset l, complete := (_ : ∀ (x : α), x ∈ List.toFinset l) }

ink

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

Equations

• Fintype.subsingleton = Fintype.subsingleton.proof_1

ink

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

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

ink

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

ink

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

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

Equations

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

ink

def Fintype.ofSurjective {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst : 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 := (_ : ∀ (b : β), b ∈ Finset.image f Finset.univ) }

ink

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

Equations

• Finset.decidableCodisjoint = decidable_of_iff (∀ ⦃a : α⦄, ¬a ∈ s → a ∈ t) (_ : (∀ ⦃a : α⦄, ¬a ∈ s → a ∈ t) ↔ Codisjoint s t)

ink

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

Equations

• Finset.decidableIsCompl = decidable_of_iff' (Disjoint s t ∧ Codisjoint s t) (_ : IsCompl s t ↔ Disjoint s t ∧ Codisjoint s t)

ink

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

The inverse of an hf : injective function f : α → β→ β, of the type ↥(Set.range f) → α↥(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

• Function.Injective.invOfMemRange hf b = Finset.choose (fun a => f a = ↑b) Finset.univ (_ : ∃! a, a ∈ Finset.univ ∧ (fun a => f a = ↑b) a)

ink

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

ink

@[simp]

theorem Function.Injective.right_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : DecidableEq β] {f : α → β} (hf : Function.Injective f) (a : α) : Function.Injective.invOfMemRange hf { val := f a, property := (_ : f a ∈ Set.range f) } = a

ink

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

ink

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

ink

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

The inverse of an embedding f : α ↪ β↪ β, of the type ↥(Set.range f) → α↥(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

• Function.Embedding.invOfMemRange f b = Function.Injective.invOfMemRange (_ : Function.Injective ↑f) b

ink

@[simp]

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

ink

@[simp]

theorem Function.Embedding.right_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : DecidableEq β] (f : α ↪ β) (a : α) : Function.Embedding.invOfMemRange f { val := ↑f a, property := (_ : ↑f a ∈ Set.range ↑f) } = a

ink

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

ink

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

ink

noncomputable def Fintype.ofInjective {α : Type u_1} {β : Type u_2} [inst : 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) (_ : Function.Surjective (Function.invFun f)) else { elems := ∅, complete := (_ : ∀ (x : α), x ∈ ∅) }

ink

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

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

Equations

• Fintype.ofEquiv α f = Fintype.ofBijective ↑f (_ : Function.Bijective ↑f)

ink

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

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

Equations

• Fintype.ofSubsingleton a = { elems := {a}, complete := (_ : ∀ (x : α), x ∈ {a}) }

ink

@[simp]

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

ink

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

Equations

• Fintype.ofIsEmpty = { elems := ∅, complete := (_ : ∀ (a : α), a ∈ ∅) }

ink

@[simp]

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

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

ink

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

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

Equations

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

ink

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

ink

@[simp]

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

ink

theorem Set.toFinset_ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) : Set.toFinset p = 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.

ink

def Set.decidableMemOfFintype {α : Type u_1} [inst : DecidableEq α] (s : Set α) [inst : 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

• Set.decidableMemOfFintype s a = decidable_of_iff (a ∈ Set.toFinset s) (_ : a ∈ Set.toFinset s ↔ a ∈ s)

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

Alias of the reverse direction of Set.toFinset_subset_toFinset.

ink

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

Alias of the reverse direction of Set.toFinset_ssubset_toFinset.

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

Equations

• Fin.fintype n = { elems := { val := ↑(List.finRange n), nodup := (_ : List.Nodup (List.finRange n)) }, complete := (_ : ∀ (a : Fin n), a ∈ List.finRange n) }

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

theorem Fin.univ_succ (n : ℕ) : Finset.univ = Finset.cons 0 (Finset.map { toFun := Fin.succ, inj' := (_ : Function.Injective Fin.succ) } Finset.univ) (_ : ¬0 ∈ Finset.map { toFun := Fin.succ, inj' := (_ : Function.Injective Fin.succ) } Finset.univ)

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

ink

theorem Fin.univ_castSucc (n : ℕ) : Finset.univ = Finset.cons (Fin.last n) (Finset.map Fin.castSucc.toEmbedding Finset.univ) (_ : ¬Fin.last n ∈ Finset.map Fin.castSucc.toEmbedding Finset.univ)

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

ink

theorem Fin.univ_succAbove (n : ℕ) (p : Fin (n + 1)) : Finset.univ = Finset.cons p (Finset.map (Fin.succAbove p).toEmbedding Finset.univ) (_ : ¬p ∈ Finset.map (Fin.succAbove p).toEmbedding Finset.univ)

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

ink

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

Equations

• Unique.fintype = Fintype.ofSubsingleton default

ink

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} (_ : ∀ (a : α), a ∈ {y} ↔ a = y)

ink

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} (_ : ∀ (a : α), a ∈ {y} ↔ y = a)

ink

theorem Fintype.univ_empty : Finset.univ = ∅

ink

theorem Fintype.univ_pempty : Finset.univ = ∅

ink

instance Unit.fintype : Fintype Unit

Equations

• Unit.fintype = Fintype.ofSubsingleton ()

ink

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

ink

instance PUnit.fintype : Fintype PUnit

Equations

• PUnit.fintype = Fintype.ofSubsingleton PUnit.unit

ink

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

ink

instance Bool.fintype : Fintype Bool

Equations

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

ink

@[simp]

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

ink

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

Equations

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

ink

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

Equations

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

ink

def Fintype.prodLeft {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : Fintype (α × β)] [inst : Nonempty β] : Fintype α

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

Equations

• Fintype.prodLeft = { elems := Finset.image Prod.fst Finset.univ, complete := (_ : ∀ (a : α), a ∈ Finset.image Prod.fst Finset.univ) }

ink

def Fintype.prodRight {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst : Fintype (α × β)] [inst : Nonempty α] : Fintype β

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

Equations

• Fintype.prodRight = { elems := Finset.image Prod.snd Finset.univ, complete := (_ : ∀ (b : β), b ∈ Finset.image Prod.snd Finset.univ) }

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• OrderDual.fintype α = inst

ink

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

Equations

• OrderDual.finite = OrderDual.finite.proof_1

ink

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

Equations

• Lex.fintype α = inst

Fintype (s : Finset α)

ink

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

Equations

• Finset.fintypeCoeSort s = { elems := Finset.attach s, complete := (_ : ∀ (x : { x // x ∈ s }), x ∈ Finset.attach s) }

ink

@[simp]

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

ink

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

ink

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

Equations

• List.Subtype.fintype l = Fintype.ofList (List.attach l) (_ : ∀ (x : { x // x ∈ l }), x ∈ List.attach l)

ink

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

Equations

• Multiset.Subtype.fintype s = Fintype.ofMultiset (Multiset.attach s) (_ : ∀ (x : { x // x ∈ s }), x ∈ Multiset.attach s)

ink

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

Equations

• Finset.Subtype.fintype s = { elems := Finset.attach s, complete := (_ : ∀ (x : { x // x ∈ s }), x ∈ Finset.attach s) }

ink

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

Equations

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

ink

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

ink

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

Equations

• PLift.fintypeProp p = { elems := if h : p then {{ down := h }} else ∅, complete := (_ : ∀ (x : PLift p), x ∈ if h : p then {{ down := h }} else ∅) }

ink

instance Prop.fintype : Fintype Prop

Equations

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

ink

@[simp]

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

ink

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

Equations

• Subtype.fintype p = Fintype.subtype (Finset.filter p Finset.univ) (_ : ∀ (a : α), a ∈ Finset.filter p Finset.univ ↔ p a)

ink

def setFintype {α : Type u_1} [inst : Fintype α] (s : Set α) [inst : 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

ink

@[simp]

theorem unitsEquivProdSubtype_symm_apply_inv (α : Type u_1) [inst : Monoid α] (p : { p // p.fst * p.snd = 1 ∧ p.snd * p.fst = 1 }) : (↑(Equiv.symm (unitsEquivProdSubtype α)) p).inv = (↑p).snd

ink

@[simp]

theorem unitsEquivProdSubtype_apply_coe (α : Type u_1) [inst : Monoid α] (u : αˣ) : ↑(↑(unitsEquivProdSubtype α) u) = (↑u, ↑u⁻¹)

ink

@[simp]

theorem unitsEquivProdSubtype_symm_apply_val (α : Type u_1) [inst : Monoid α] (p : { p // p.fst * p.snd = 1 ∧ p.snd * p.fst = 1 }) : ↑(↑(Equiv.symm (unitsEquivProdSubtype α)) p) = (↑p).fst

ink

def unitsEquivProdSubtype (α : Type u_1) [inst : Monoid α] : αˣ ≃ { p // p.fst * p.snd = 1 ∧ p.snd * p.fst = 1 }

The αˣ type is equivalent to a subtype of α × α× α.

Equations

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

ink

@[simp]

theorem unitsEquivNeZero_symm_apply (α : Type u_1) [inst : GroupWithZero α] (a : { a // a ≠ 0 }) : ↑(Equiv.symm (unitsEquivNeZero α)) a = Units.mk0 ↑a (_ : ↑a ≠ 0)

ink

@[simp]

theorem unitsEquivNeZero_apply_coe (α : Type u_1) [inst : GroupWithZero α] (a : αˣ) : ↑(↑(unitsEquivNeZero α) a) = ↑a

ink

def unitsEquivNeZero (α : Type u_1) [inst : GroupWithZero α] : αˣ ≃ { a // a ≠ 0 }

In a GroupWithZero α, the unit group αˣ is equivalent to the subtype of nonzero elements.

Equations

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

ink

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

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• Quotient.fintype s = Fintype.ofSurjective Quotient.mk'' (_ : ∀ (x : Quotient s), ∃ a, Quotient.mk'' a = x)

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

ink

def Fintype.chooseX {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst : 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 = { val := Finset.choose p Finset.univ (_ : ∃! a, a ∈ Finset.univ ∧ p a), property := Fintype.chooseX.proof_2 p hp }

ink

def Fintype.choose {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst : 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)

ink

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

ink

theorem Fintype.choose_subtype_eq {α : Type u_1} (p : α → Prop) [inst : Fintype { a // p a }] [inst : DecidableEq α] (x : { a // p a }) (h : optParam (∃! a, ↑a = ↑x) (_ : ∃ x, (fun a => ↑a = ↑x) x ∧ ∀ (y : { a // p a }), (fun a => ↑a = ↑x) y → y = x)) : Fintype.choose (fun y => ↑y = ↑x) h = x

ink

def Fintype.bijInv {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : 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) (_ : ∃! a, (fun a => f a = b) a)

ink

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

ink

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

ink

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

ink

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

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

Equations

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

ink

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

A Nonempty Fintype constructively contains an element.

Equations

• truncOfNonemptyFintype α = truncOfMultisetExistsMem Finset.univ.val (_ : ∃ x, x ∈ Finset.univ.val)

ink

def truncSigmaOfExists {α : Type u_1} [inst : Fintype α] {P : α → Prop} [inst : 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∃ a, P a to Trunc (Σ' a, P a), containing data.

Equations

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

ink

@[simp]

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

ink

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

Auxiliary definition to show exists_seq_of_forall_finset_exists.

Equations

• seqOfForallFinsetExistsAux P r h x = Classical.choose (h (Finset.image (fun i => seqOfForallFinsetExistsAux P r h ↑i) Finset.univ))

ink

theorem exists_seq_of_forall_finset_exists {α : Type u_1} (P : α → Prop) (r : α → α → Prop) (h : ∀ (s : Finset α), ((x : α) → x ∈ s → P x) → ∃ y, P y ∧ ((x : α) → 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.

ink

theorem exists_seq_of_forall_finset_exists' {α : Type u_1} (P : α → Prop) (r : α → α → Prop) [inst : IsSymm α r] (h : ∀ (s : Finset α), ((x : α) → x ∈ s → P x) → ∃ y, P y ∧ ((x : α) → 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 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≠ n. We also ensure that all constructed points satisfy a given predicate P.