Documentation

Mathlib.Data.Fintype.Basic

Finite types #

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

Main declarations #

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

Instances #

Instances for Fintype for

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.

source
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
source
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
source
@[simp]
theorem Finset.mem_univ {α : Type u_1} [Fintype α] (x : α) :
x ∈ Finset.univ
source
theorem Finset.mem_univ_val {α : Type u_1} [Fintype α] (x : α) :
x ∈ Finset.univ.val
source
theorem Finset.eq_univ_iff_forall {α : Type u_1} [Fintype α] {s : Finset α} :
s = Finset.univ ↔ ∀ (x : α), x ∈ s
source
theorem Finset.eq_univ_of_forall {α : Type u_1} [Fintype α] {s : Finset α} :
(∀ (x : α), x ∈ s) → s = Finset.univ
source
@[simp]
theorem Finset.coe_univ {α : Type u_1} [Fintype α] :
↑Finset.univ = Set.univ
source
@[simp]
theorem Finset.coe_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} :
↑s = Set.univ ↔ s = Finset.univ
source
theorem Finset.Nonempty.eq_univ {α : Type u_1} [Fintype α] {s : Finset α} [Subsingleton α] :
s.Nonempty → s = Finset.univ
source
theorem Finset.univ_nonempty_iff {α : Type u_1} [Fintype α] :
Finset.univ.Nonempty ↔ Nonempty α
source
theorem Finset.univ_nonempty {α : Type u_1} [Fintype α] [Nonempty α] :
Finset.univ.Nonempty
source
theorem Finset.univ_eq_empty_iff {α : Type u_1} [Fintype α] :
Finset.univ = ∅ ↔ IsEmpty α
source
@[simp]
theorem Finset.univ_eq_empty {α : Type u_1} [Fintype α] [IsEmpty α] :
Finset.univ = ∅
source
@[simp]
theorem Finset.univ_unique {α : Type u_1} [Fintype α] [Unique α] :
Finset.univ = {default}
source
@[simp]
theorem Finset.subset_univ {α : Type u_1} [Fintype α] (s : Finset α) :
s ⊆ Finset.univ
source
instance Finset.boundedOrder {α : Type u_1} [Fintype α] :
BoundedOrder (Finset α)
Equations
source
@[simp]
theorem Finset.top_eq_univ {α : Type u_1} [Fintype α] :
⊤ = Finset.univ
source
theorem Finset.ssubset_univ_iff {α : Type u_1} [Fintype α] {s : Finset α} :
s ⊂ Finset.univ ↔ s ≠ Finset.univ
source
@[simp]
theorem Finset.univ_subset_iff {α : Type u_1} [Fintype α] {s : Finset α} :
Finset.univ ⊆ s ↔ s = Finset.univ
source
theorem Finset.codisjoint_left {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} :
Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t
source
theorem Finset.codisjoint_right {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} :
Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∈ s
source
instance Finset.booleanAlgebra {α : Type u_1} [Fintype α] [DecidableEq α] :
BooleanAlgebra (Finset α)
Equations
  • Finset.booleanAlgebra = GeneralizedBooleanAlgebra.toBooleanAlgebra
source
theorem Finset.sdiff_eq_inter_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) :
s \ t = s ∩ tᶜ
source
theorem Finset.compl_eq_univ_sdiff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
sᶜ = Finset.univ \ s
source
@[simp]
theorem Finset.mem_compl {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} :
a ∈ sᶜ ↔ a ∉ s
source
theorem Finset.not_mem_compl {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} :
a ∉ sᶜ ↔ a ∈ s
source
@[simp]
theorem Finset.coe_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
↑sᶜ = (↑s)ᶜ
source
@[simp]
theorem Finset.compl_subset_compl {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] :
sᶜ ⊆ tᶜ ↔ t ⊆ s
source
@[simp]
theorem Finset.compl_ssubset_compl {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] :
sᶜ ⊂ tᶜ ↔ t ⊂ s
source
theorem Finset.subset_compl_comm {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] :
s ⊆ tᶜ ↔ t ⊆ sᶜ
source
@[simp]
theorem Finset.subset_compl_singleton {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} :
s ⊆ {a}ᶜ ↔ a ∉ s
source
@[simp]
theorem Finset.compl_empty {α : Type u_1} [Fintype α] [DecidableEq α] :
∅ᶜ = Finset.univ
source
@[simp]
theorem Finset.compl_univ {α : Type u_1} [Fintype α] [DecidableEq α] :
Finset.univᶜ = ∅
source
@[simp]
theorem Finset.compl_eq_empty_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
sᶜ = ∅ ↔ s = Finset.univ
source
@[simp]
theorem Finset.compl_eq_univ_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
sᶜ = Finset.univ ↔ s = ∅
source
@[simp]
theorem Finset.union_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
s ∪ sᶜ = Finset.univ
source
@[simp]
theorem Finset.inter_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
s ∩ sᶜ = ∅
source
@[simp]
theorem Finset.compl_union {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) :
(s ∪ t)ᶜ = sᶜ ∩ tᶜ
source
@[simp]
theorem Finset.compl_inter {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (t : Finset α) :
(s ∩ t)ᶜ = sᶜ ∪ tᶜ
source
@[simp]
theorem Finset.compl_erase {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} :
(Finset.erase s a)ᶜ = insert a sᶜ
source
@[simp]
theorem Finset.compl_insert {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} :
(insert a s)ᶜ = Finset.erase sᶜ a
source
theorem Finset.insert_compl_insert {α : Type u_1} [Fintype α] {s : Finset α} [DecidableEq α] {a : α} (ha : a ∉ s) :
insert a (insert a s)ᶜ = sᶜ
source
@[simp]
theorem Finset.insert_compl_self {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) :
insert x {x}ᶜ = Finset.univ
source
@[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
source
theorem Finset.compl_ne_univ_iff_nonempty {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
sᶜ ≠ Finset.univ ↔ s.Nonempty
source
theorem Finset.compl_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (a : α) :
{a}ᶜ = Finset.erase Finset.univ a
source
theorem Finset.insert_inj_on' {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
Set.InjOn (fun (a : α) => insert a s) ↑sᶜ
source
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
source
@[simp]
theorem Finset.image_univ_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] (f : β ≃ α) :
Finset.image (⇑f) Finset.univ = Finset.univ
source
@[simp]
theorem Finset.univ_inter {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
Finset.univ ∩ s = s
source
@[simp]
theorem Finset.inter_univ {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
s ∩ Finset.univ = s
source
@[simp]
theorem Finset.inter_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} {t : Finset α} [DecidableEq α] :
s ∩ t = Finset.univ ↔ s = Finset.univ ∧ t = Finset.univ
source
theorem Finset.singleton_eq_univ {α : Type u_1} [Fintype α] [Subsingleton α] (a : α) :
{a} = Finset.univ
source
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
source
@[simp]
theorem Finset.map_univ_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : β ≃ α) :
Finset.map (Equiv.toEmbedding f) Finset.univ = Finset.univ
source
@[simp]
theorem Finset.piecewise_univ {α : Type u_1} [Fintype α] [(i : α) → Decidable (i ∈ Finset.univ)] {δ : α → Sort u_4} (f : (i : α) → δ i) (g : (i : α) → δ i) :
Finset.piecewise Finset.univ f g = f
source
theorem Finset.piecewise_compl {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) [(i : α) → Decidable (i ∈ s)] [(i : α) → Decidable (i ∈ sᶜ)] {δ : α → Sort u_4} (f : (i : α) → δ i) (g : (i : α) → δ i) :
Finset.piecewise sᶜ f g = Finset.piecewise s g f
source
@[simp]
theorem Finset.piecewise_erase_univ {α : Type u_1} [Fintype α] {δ : α → Sort u_4} [DecidableEq α] (a : α) (f : (a : α) → δ a) (g : (a : α) → δ a) :
Finset.piecewise (Finset.erase Finset.univ a) f g = Function.update f a (g a)
source
theorem Finset.univ_map_equiv_to_embedding {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (e : α ≃ β) :
Finset.map (Equiv.toEmbedding e) Finset.univ = Finset.univ
source
@[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
source
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.

source
theorem Finset.coe_filter_univ {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] :
↑(Finset.filter p Finset.univ) = {x : α | p x}
source
@[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
source
@[simp]
theorem Finset.subtype_univ {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a : α // p a }] :
Finset.subtype p Finset.univ = Finset.univ
source
instance Fintype.decidablePiFintype {α : Type u_5} {β : α → Type u_4} [(a : α) → DecidableEq (β a)] [Fintype α] :
DecidableEq ((a : α) → β a)
Equations
source
instance Fintype.decidableForallFintype {α : Type u_1} {p : α → Prop} [DecidablePred p] [Fintype α] :
Decidable (∀ (a : α), p a)
Equations
source
instance Fintype.decidableExistsFintype {α : Type u_1} {p : α → Prop} [DecidablePred p] [Fintype α] :
Decidable (∃ (a : α), p a)
Equations
source
instance Fintype.decidableMemRangeFintype {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α → β) :
DecidablePred fun (x : β) => x ∈ Set.range f
Equations
source
instance Fintype.decidableSubsingleton {α : Type u_1} [Fintype α] [DecidableEq α] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] :
Decidable (Set.Subsingleton s)
Equations
source
instance Fintype.decidableEqEquivFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] :
DecidableEq (α ≃ β)
Equations
source
instance Fintype.decidableEqEmbeddingFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] :
DecidableEq (α ↪ β)
Equations
source
instance Fintype.decidableEqZeroHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Zero α] [Zero β] :
DecidableEq (ZeroHom α β)
Equations
source
theorem Fintype.decidableEqZeroHomFintype.proof_1 {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] (a : ZeroHom α β) (b : ZeroHom α β) :
⇑a = ⇑b ↔ a = b
source
instance Fintype.decidableEqOneHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [One α] [One β] :
DecidableEq (OneHom α β)
Equations
source
instance Fintype.decidableEqAddHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Add α] [Add β] :
DecidableEq (AddHom α β)
Equations
source
theorem Fintype.decidableEqAddHomFintype.proof_1 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (a : AddHom α β) (b : AddHom α β) :
⇑a = ⇑b ↔ a = b
source
instance Fintype.decidableEqMulHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Mul α] [Mul β] :
DecidableEq (α →ₙ* β)
Equations
source
instance Fintype.decidableEqAddMonoidHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [AddZeroClass α] [AddZeroClass β] :
DecidableEq (α →+ β)
Equations
source
theorem Fintype.decidableEqAddMonoidHomFintype.proof_1 {α : Type u_1} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] (a : α →+ β) (b : α →+ β) :
⇑a = ⇑b ↔ a = b
source
instance Fintype.decidableEqMonoidHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [MulOneClass α] [MulOneClass β] :
DecidableEq (α →* β)
Equations
source
instance Fintype.decidableEqMonoidWithZeroHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [MulZeroOneClass α] [MulZeroOneClass β] :
DecidableEq (α →*₀ β)
Equations
source
instance Fintype.decidableEqRingHomFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Semiring α] [Semiring β] :
DecidableEq (α →+* β)
Equations
source
instance Fintype.decidableInjectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] :
DecidablePred Function.Injective
Equations
source
instance Fintype.decidableSurjectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Fintype β] :
DecidablePred Function.Surjective
Equations
source
instance Fintype.decidableBijectiveFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] :
DecidablePred Function.Bijective
Equations
source
instance Fintype.decidableRightInverseFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] (f : α → β) (g : β → α) :
Decidable (Function.RightInverse f g)
Equations
source
instance Fintype.decidableLeftInverseFintype {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype β] (f : α → β) (g : β → α) :
Decidable (Function.LeftInverse f g)
Equations
source
def Fintype.ofMultiset {α : Type u_1} [DecidableEq α] (s : Multiset α) (H : ∀ (x : α), x ∈ s) :
Fintype α

Construct a proof of Fintype α from a universal multiset

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

Construct a proof of Fintype α from a universal list

Equations
source
instance Fintype.subsingleton (α : Type u_4) :
Subsingleton (Fintype α)
Equations
  • ⋯ = ⋯
source
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
source
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
source
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
source
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
source
@[simp]
theorem Finset.filter_univ_mem {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
Finset.filter (fun (x : α) => x ∈ s) Finset.univ = s
source
instance Finset.decidableCodisjoint {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} {t : Finset α} :
Decidable (Codisjoint s t)
Equations
source
instance Finset.decidableIsCompl {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} {t : Finset α} :
Decidable (IsCompl s t)
Equations
source
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
source
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 (Function.Injective.invOfMemRange hf b) = ↑b
source
@[simp]
theorem Function.Injective.right_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (a : α) :
Function.Injective.invOfMemRange hf { val := f a, property := ⋯ } = a
source
theorem Function.Injective.invFun_restrict {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) [Nonempty α] :
Set.restrict (Set.range f) (Function.invFun f) = Function.Injective.invOfMemRange hf
source
theorem Function.Injective.invOfMemRange_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) :
Function.Surjective (Function.Injective.invOfMemRange hf)
source
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
source
@[simp]
theorem Function.Embedding.left_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) (b : ↑(Set.range ⇑f)) :
f (Function.Embedding.invOfMemRange f b) = ↑b
source
@[simp]
theorem Function.Embedding.right_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) (a : α) :
Function.Embedding.invOfMemRange f { val := f a, property := ⋯ } = a
source
theorem Function.Embedding.invFun_restrict {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) [Nonempty α] :
Set.restrict (Set.range ⇑f) (Function.invFun ⇑f) = Function.Embedding.invOfMemRange f
source
theorem Function.Embedding.invOfMemRange_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) :
Function.Surjective (Function.Embedding.invOfMemRange f)
source
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
source
def Fintype.ofEquiv {β : Type u_2} (α : Type u_4) [Fintype α] (f : α ≃ β) :
Fintype β

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

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

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

Equations
source
@[simp]
theorem Fintype.univ_ofSubsingleton {α : Type u_1} (a : α) [Subsingleton α] :
Finset.univ = {a}
source
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 := ⋯ }
source
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.

source
instance Fintype.instFintypeEmpty :
Fintype Empty
Equations
source
instance Fintype.instFintypePEmpty :
Fintype PEmpty.{u_4 + 1}
Equations
source
def Set.toFinset {α : Type u_1} (s : Set α) [Fintype ↑s] :
Finset α

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

Equations
source
theorem Set.toFinset_congr {α : Type u_1} {s : Set α} {t : Set α} [Fintype ↑s] [Fintype ↑t] (h : s = t) :
Set.toFinset s = Set.toFinset t
source
@[simp]
theorem Set.mem_toFinset {α : Type u_1} {s : Set α} [Fintype ↑s] {a : α} :
a ∈ Set.toFinset s ↔ a ∈ s
source
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.

source
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
source
@[simp]
theorem Set.coe_toFinset {α : Type u_1} (s : Set α) [Fintype ↑s] :
↑(Set.toFinset s) = s
source
@[simp]
theorem Set.toFinset_nonempty {α : Type u_1} {s : Set α} [Fintype ↑s] :
(Set.toFinset s).Nonempty ↔ Set.Nonempty s
source
@[simp]
theorem Set.toFinset_inj {α : Type u_1} {s : Set α} {t : Set α} [Fintype ↑s] [Fintype ↑t] :
Set.toFinset s = Set.toFinset t ↔ s = t
source
theorem Set.toFinset_subset_toFinset {α : Type u_1} {s : Set α} {t : Set α} [Fintype ↑s] [Fintype ↑t] :
Set.toFinset s ⊆ Set.toFinset t ↔ s ⊆ t
source
@[simp]
theorem Set.toFinset_ssubset {α : Type u_1} {s : Set α} [Fintype ↑s] {t : Finset α} :
Set.toFinset s ⊂ t ↔ s ⊂ ↑t
source
@[simp]
theorem Set.subset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype ↑t] :
s ⊆ Set.toFinset t ↔ ↑s ⊆ t
source
@[simp]
theorem Set.ssubset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype ↑t] :
s ⊂ Set.toFinset t ↔ ↑s ⊂ t
source
theorem Set.toFinset_ssubset_toFinset {α : Type u_1} {s : Set α} {t : Set α} [Fintype ↑s] [Fintype ↑t] :
Set.toFinset s ⊂ Set.toFinset t ↔ s ⊂ t
source
@[simp]
theorem Set.toFinset_subset {α : Type u_1} {s : Set α} [Fintype ↑s] {t : Finset α} :
Set.toFinset s ⊆ t ↔ s ⊆ ↑t
source
theorem Set.toFinset_mono {α : Type u_1} {s : Set α} {t : Set α} [Fintype ↑s] [Fintype ↑t] :
s ⊆ t → Set.toFinset s ⊆ Set.toFinset t

Alias of the reverse direction of Set.toFinset_subset_toFinset.

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

Alias of the reverse direction of Set.toFinset_ssubset_toFinset.

source
@[simp]
theorem Set.disjoint_toFinset {α : Type u_1} {s : Set α} {t : Set α} [Fintype ↑s] [Fintype ↑t] :
Disjoint (Set.toFinset s) (Set.toFinset t) ↔ Disjoint s t
source
@[simp]
theorem Set.toFinset_inter {α : Type u_1} (s : Set α) (t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s ∩ t)] :
Set.toFinset (s ∩ t) = Set.toFinset s ∩ Set.toFinset t
source
@[simp]
theorem Set.toFinset_union {α : Type u_1} (s : Set α) (t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s ∪ t)] :
Set.toFinset (s ∪ t) = Set.toFinset s ∪ Set.toFinset t
source
@[simp]
theorem Set.toFinset_diff {α : Type u_1} (s : Set α) (t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s \ t)] :
Set.toFinset (s \ t) = Set.toFinset s \ Set.toFinset t
source
@[simp]
theorem Set.toFinset_symmDiff {α : Type u_1} (s : Set α) (t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(symmDiff s t)] :
Set.toFinset (symmDiff s t) = symmDiff (Set.toFinset s) (Set.toFinset t)
source
@[simp]
theorem Set.toFinset_compl {α : Type u_1} (s : Set α) [DecidableEq α] [Fintype ↑s] [Fintype α] [Fintype ↑sᶜ] :
Set.toFinset sᶜ = (Set.toFinset s)ᶜ
source
@[simp]
theorem Set.toFinset_empty {α : Type u_1} [Fintype ↑∅] :
Set.toFinset ∅ = ∅
source
@[simp]
theorem Set.toFinset_univ {α : Type u_1} [Fintype α] [Fintype ↑Set.univ] :
Set.toFinset Set.univ = Finset.univ
source
@[simp]
theorem Set.toFinset_eq_empty {α : Type u_1} {s : Set α} [Fintype ↑s] :
Set.toFinset s = ∅ ↔ s = ∅
source
@[simp]
theorem Set.toFinset_eq_univ {α : Type u_1} {s : Set α} [Fintype α] [Fintype ↑s] :
Set.toFinset s = Finset.univ ↔ s = Set.univ
source
@[simp]
theorem Set.toFinset_setOf {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype ↑{x : α | p x}] :
Set.toFinset {x : α | p x} = Finset.filter p Finset.univ
source
theorem Set.toFinset_ssubset_univ {α : Type u_1} [Fintype α] {s : Set α} [Fintype ↑s] :
Set.toFinset s ⊂ Finset.univ ↔ s ⊂ Set.univ
source
@[simp]
theorem Set.toFinset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Set α) [Fintype ↑s] [Fintype ↑(f '' s)] :
Set.toFinset (f '' s) = Finset.image f (Set.toFinset s)
source
@[simp]
theorem Set.toFinset_range {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] (f : β → α) [Fintype ↑(Set.range f)] :
Set.toFinset (Set.range f) = Finset.image f Finset.univ
source
@[simp]
theorem Set.toFinset_singleton {α : Type u_1} (a : α) [Fintype ↑{a}] :
Set.toFinset {a} = {a}
source
@[simp]
theorem Set.toFinset_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Set α} [Fintype ↑(insert a s)] [Fintype ↑s] :
Set.toFinset (insert a s) = insert a (Set.toFinset s)
source
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 = Set.toFinset s
source
@[simp]
theorem Finset.toFinset_coe {α : Type u_1} (s : Finset α) [Fintype ↑↑s] :
Set.toFinset ↑s = s
source
instance Fin.fintype (n : ℕ) :
Fintype (Fin n)
Equations
source
theorem Fin.univ_def (n : ℕ) :
Finset.univ = { val := ↑(List.finRange n), nodup := ⋯ }
source
@[simp]
theorem List.toFinset_finRange (n : ℕ) :
List.toFinset (List.finRange n) = Finset.univ
source
@[simp]
theorem Fin.image_succAbove_univ {n : ℕ} (i : Fin (n + 1)) :
Finset.image (Fin.succAbove i) Finset.univ = {i}ᶜ
source
@[simp]
theorem Fin.image_succ_univ (n : ℕ) :
Finset.image Fin.succ Finset.univ = {0}ᶜ
source
@[simp]
theorem Fin.image_castSucc (n : ℕ) :
Finset.image Fin.castSucc Finset.univ = {Fin.last n}ᶜ
source
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

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

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

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

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

source
instance Unique.fintype {α : Type u_4} [Unique α] :
Fintype α
Equations
source
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
source
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
source
theorem Fintype.univ_empty :
Finset.univ = ∅
source
theorem Fintype.univ_pempty :
Finset.univ = ∅
source
instance Unit.fintype :
Fintype Unit
Equations
source
theorem Fintype.univ_unit :
Finset.univ = {()}
source
instance PUnit.fintype :
Fintype PUnit.{u_4 + 1}
Equations
source
theorem Fintype.univ_punit :
Finset.univ = {PUnit.unit}
source
instance Bool.fintype :
Fintype Bool
Equations
source
@[simp]
theorem Fintype.univ_bool :
Finset.univ = {true, false}
source
instance Additive.fintype {α : Type u_1} [Fintype α] :
Fintype (Additive α)
Equations
source
instance Multiplicative.fintype {α : Type u_1} [Fintype α] :
Fintype (Multiplicative α)
Equations
source
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 := ⋯ }
source
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 := ⋯ }
source
instance ULift.fintype (α : Type u_4) [Fintype α] :
Fintype (ULift.{u_5, u_4} α)
Equations
source
instance PLift.fintype (α : Type u_4) [Fintype α] :
Fintype (PLift α)
Equations
source
instance OrderDual.fintype (α : Type u_4) [Fintype α] :
Fintype αᵒᵈ
Equations
source
instance OrderDual.finite (α : Type u_4) [Finite α] :
Finite αᵒᵈ
Equations
  • ⋯ = inst
source
instance Lex.fintype (α : Type u_4) [Fintype α] :
Fintype (Lex α)
Equations

Fintype (s : Finset α) #

source
instance Finset.fintypeCoeSort {α : Type u} (s : Finset α) :
Fintype { x : α // x ∈ s }
Equations
source
@[simp]
theorem Finset.univ_eq_attach {α : Type u} (s : Finset α) :
Finset.univ = Finset.attach s
source
theorem Fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} :
↑(Finset.image f Finset.univ) = Set.range f
source
instance List.Subtype.fintype {α : Type u_1} [DecidableEq α] (l : List α) :
Fintype { x : α // x ∈ l }
Equations
source
instance Multiset.Subtype.fintype {α : Type u_1} [DecidableEq α] (s : Multiset α) :
Fintype { x : α // x ∈ s }
Equations
source
instance Finset.Subtype.fintype {α : Type u_1} (s : Finset α) :
Fintype { x : α // x ∈ s }
Equations
source
instance FinsetCoe.fintype {α : Type u_1} (s : Finset α) :
Fintype ↑↑s
Equations
source
theorem Finset.attach_eq_univ {α : Type u_1} {s : Finset α} :
Finset.attach s = Finset.univ
source
instance PLift.fintypeProp (p : Prop) [Decidable p] :
Fintype (PLift p)
Equations
source
instance Prop.fintype :
Fintype Prop
Equations
source
@[simp]
theorem Fintype.univ_Prop :
Finset.univ = {True, False}
source
instance Subtype.fintype {α : Type u_1} (p : α → Prop) [DecidablePred p] [Fintype α] :
Fintype { x : α // p x }
Equations
source
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
source
@[simp]
theorem unitsEquivProdSubtype_apply_coe (α : Type u_1) [Monoid α] (u : αˣ) :
↑((unitsEquivProdSubtype α) u) = (↑u, ↑u⁻¹)
source
@[simp]
theorem val_unitsEquivProdSubtype_symm_apply (α : Type u_1) [Monoid α] (p : { p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }) :
↑((unitsEquivProdSubtype α).symm p) = (↑p).1
source
@[simp]
theorem val_inv_unitsEquivProdSubtype_symm_apply (α : Type u_1) [Monoid α] (p : { p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }) :
↑((unitsEquivProdSubtype α).symm p)⁻¹ = (↑p).2
source
def unitsEquivProdSubtype (α : Type u_1) [Monoid α] :
αˣ ≃ { p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem unitsEquivNeZero_symm_apply (α : Type u_1) [GroupWithZero α] (a : { a : α // a ≠ 0 }) :
(unitsEquivNeZero α).symm a = Units.mk0 ↑a ⋯
source
@[simp]
theorem unitsEquivNeZero_apply_coe (α : Type u_1) [GroupWithZero α] (a : αˣ) :
↑((unitsEquivNeZero α) a) = ↑a
source
def unitsEquivNeZero (α : Type u_1) [GroupWithZero α] :
αˣ ≃ { a : α // a ≠ 0 }

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

Equations
  • unitsEquivNeZero α = { toFun := fun (a : αˣ) => { val := ↑a, property := ⋯ }, invFun := fun (a : { a : α // a ≠ 0 }) => Units.mk0 ↑a ⋯, left_inv := ⋯, right_inv := ⋯ }
source
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 α) => Set.toFinset s, left_inv := ⋯, right_inv := ⋯ }
source
@[simp]
theorem Fintype.coe_finsetEquivSet {α : Type u_1} [Fintype α] :
⇑Fintype.finsetEquivSet = Finset.toSet
source
@[simp]
theorem Fintype.finsetEquivSet_apply {α : Type u_1} [Fintype α] (s : Finset α) :
Fintype.finsetEquivSet s = ↑s
source
@[simp]
theorem Fintype.finsetEquivSet_symm_apply {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] :
Fintype.finsetEquivSet.symm s = Set.toFinset s
source
@[simp]
theorem Fintype.finsetOrderIsoSet_toEquiv {α : Type u_1} [Fintype α] :
Fintype.finsetOrderIsoSet.toEquiv = Fintype.finsetEquivSet
source
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' := ⋯ }
source
@[simp]
theorem Fintype.coe_finsetOrderIsoSet {α : Type u_1} [Fintype α] :
⇑Fintype.finsetOrderIsoSet = Finset.toSet
source
@[simp]
theorem Fintype.coe_finsetOrderIsoSet_symm {α : Type u_1} [Fintype α] :
⇑(OrderIso.symm Fintype.finsetOrderIsoSet) = ⇑Fintype.finsetEquivSet.symm
source
instance Quotient.fintype {α : Type u_1} [Fintype α] (s : Setoid α) [DecidableRel fun (x x_1 : α) => x ≈ x_1] :
Fintype (Quotient s)
Equations
source
instance PSigma.fintypePropLeft {α : Prop} {β : α → Type u_4} [Decidable α] [(a : α) → Fintype (β a)] :
Fintype ((a : α) ×' β a)
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
instance PSigma.fintypePropProp {α : Prop} {β : α → Prop} [Decidable α] [(a : α) → Decidable (β a)] :
Fintype ((a : α) ×' β a)
Equations
  • PSigma.fintypePropProp = if h : ∃ (a : α), β a then { elems := {{ fst := ⋯, snd := ⋯ }}, complete := ⋯ } else { elems := ∅, complete := ⋯ }
source
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.
source
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
source
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
source
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
source
theorem Fintype.choose_spec {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (hp : ∃! (a : α), p a) :
p (Fintype.choose p hp)
source
theorem Fintype.choose_subtype_eq {α : Type u_4} (p : α → Prop) [Fintype { a : α // p a }] [DecidableEq α] (x : { a : α // p a }) (h : optParam (∃! (a : { a : α // p a }), ↑a = ↑x) ⋯) :
Fintype.choose (fun (y : { a : α // p a }) => ↑y = ↑x) h = x
source
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
source
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
source
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
source
theorem Fintype.bijective_bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (f_bij : Function.Bijective f) :
Function.Bijective (Fintype.bijInv f_bij)
source
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.
source
def truncOfNonemptyFintype (α : Type u_4) [Nonempty α] [Fintype α] :
Trunc α

A Nonempty Fintype constructively contains an element.

Equations
source
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
source
@[simp]
theorem Multiset.count_univ {α : Type u_1} [Fintype α] [DecidableEq α] (a : α) :
Multiset.count a Finset.univ.val = 1
source
@[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
source
@[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.

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

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