Equivalences between Fintype, Fin and Finite

This file defines the bijection between a Fintype α and Fin (Fintype.card α), and uses this to relate Fintype with Finite. From that we can derive properties of Finite and Infinite, and show some instances of Infinite.

Main declarations

• Fintype.truncEquivFin: A fintype α is computably equivalent to Fin (card α). The Trunc-free, noncomputable version is Fintype.equivFin.
• Fintype.truncEquivOfCardEq Fintype.equivOfCardEq: Two fintypes of same cardinality are equivalent. See above.
• Fin.equiv_iff_eq: Fin m ≃ Fin n iff m = n.
• Infinite.natEmbedding: An embedding of ℕ into an infinite type.

Types which have an injection from/a surjection to an Infinite type are themselves Infinite. See Infinite.of_injective and Infinite.of_surjective.

Instances

We provide Infinite instances for

• specific types: ℕ, ℤ, String
• type constructors: Multiset α, List α

def Fintype.truncEquivFin (α : Type u_4) [DecidableEq α] [Fintype α] : Trunc (α ≃ Fin (card α))

There is (computably) an equivalence between α and Fin (card α).

Since it is not unique and depends on which permutation of the universe list is used, the equivalence is wrapped in Trunc to preserve computability.

See Fintype.equivFin for the noncomputable version, and Fintype.truncEquivFinOfCardEq and Fintype.equivFinOfCardEq for an equiv α ≃ Fin n given Fintype.card α = n.

See Fintype.truncFinBijection for a version without [DecidableEq α].

Equations

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

noncomputable def Fintype.equivFin (α : Type u_4) [Fintype α] : α ≃ Fin (card α)

There is (noncomputably) an equivalence between α and Fin (card α).

See Fintype.truncEquivFin for the computable version, and Fintype.truncEquivFinOfCardEq and Fintype.equivFinOfCardEq for an equiv α ≃ Fin n given Fintype.card α = n.

Equations

• Fintype.equivFin α = (Fintype.truncEquivFin α).out

def Fintype.truncFinBijection (α : Type u_4) [Fintype α] : Trunc { f : Fin (card α) → α // Function.Bijective f }

There is (computably) a bijection between Fin (card α) and α.

Since it is not unique and depends on which permutation of the universe list is used, the bijection is wrapped in Trunc to preserve computability.

See Fintype.truncEquivFin for a version that gives an equivalence given [DecidableEq α].

Equations

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

def Fintype.truncEquivFinOfCardEq {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (h : card α = n) : Trunc (α ≃ Fin n)

If the cardinality of α is n, there is computably a bijection between α and Fin n.

See Fintype.equivFinOfCardEq for the noncomputable definition, and Fintype.truncEquivFin and Fintype.equivFin for the bijection α ≃ Fin (card α).

Equations

• Fintype.truncEquivFinOfCardEq h = Trunc.map (fun (e : α ≃ Fin (Fintype.card α)) => e.trans (finCongr h)) (Fintype.truncEquivFin α)

noncomputable def Fintype.equivFinOfCardEq {α : Type u_1} [Fintype α] {n : ℕ} (h : card α = n) : α ≃ Fin n

If the cardinality of α is n, there is noncomputably a bijection between α and Fin n.

See Fintype.truncEquivFinOfCardEq for the computable definition, and Fintype.truncEquivFin and Fintype.equivFin for the bijection α ≃ Fin (card α).

Equations

• Fintype.equivFinOfCardEq h = (Fintype.truncEquivFinOfCardEq h).out

def Fintype.truncEquivOfCardEq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (h : card α = card β) : Trunc (α ≃ β)

Two Fintypes with the same cardinality are (computably) in bijection.

See Fintype.equivOfCardEq for the noncomputable version, and Fintype.truncEquivFinOfCardEq and Fintype.equivFinOfCardEq for the specialization to Fin.

Equations

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

noncomputable def Fintype.equivOfCardEq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (h : card α = card β) : α ≃ β

Two Fintypes with the same cardinality are (noncomputably) in bijection.

See Fintype.truncEquivOfCardEq for the computable version, and Fintype.truncEquivFinOfCardEq and Fintype.equivFinOfCardEq for the specialization to Fin.

Equations

• Fintype.equivOfCardEq h = (Fintype.truncEquivOfCardEq h).out

theorem Fintype.card_eq {α : Type u_4} {β : Type u_5} [_F : Fintype α] [_G : Fintype β] : card α = card β ↔ Nonempty (α ≃ β)

Relation to Finite

In this section we prove that α : Type* is Finite if and only if Fintype α is nonempty.

theorem Fintype.finite {α : Type u_4} (_inst : Fintype α) : Finite α

@[instance 900]

instance Finite.of_fintype (α : Type u_4) [Fintype α] : Finite α

For efficiency reasons, we want Finite instances to have higher priority than ones coming from Fintype instances.

theorem finite_iff_nonempty_fintype (α : Type u_4) : Finite α ↔ Nonempty (Fintype α)

noncomputable def Fintype.ofFinite (α : Type u_4) [Finite α] : Fintype α

Noncomputably get a Fintype instance from a Finite instance. This is not an instance because we want Fintype instances to be useful for computations.

Equations

• Fintype.ofFinite α = ⋯.some

theorem Finite.of_injective {α : Sort u_4} {β : Sort u_5} [Finite β] (f : α → β) (H : Function.Injective f) : Finite α

@[instance 100]

instance Finite.of_subsingleton {α : Sort u_4} [Subsingleton α] : Finite α

instance prop (p : Prop) : Finite p

instance Subtype.finite {α : Sort u_4} [Finite α] {p : α → Prop} : Finite { x : α // p x }

This instance also provides [Finite s] for s : Set α.

theorem Finite.of_surjective {α : Sort u_4} {β : Sort u_5} [Finite α] (f : α → β) (H : Function.Surjective f) : Finite β

instance Quot.finite {α : Sort u_4} [Finite α] (r : α → α → Prop) : Finite (Quot r)

instance Quotient.finite {α : Sort u_4} [Finite α] (s : Setoid α) : Finite (Quotient s)

theorem Fintype.card_eq_one_iff {α : Type u_1} [Fintype α] : card α = 1 ↔ ∃ (x : α), ∀ (y : α), y = x

theorem Fintype.card_eq_one_iff_nonempty_unique {α : Type u_1} [Fintype α] : card α = 1 ↔ Nonempty (Unique α)

instance Fintype.instNeZeroNatCardOfNonempty_1 {α : Type u_1} [Fintype α] [Nonempty α] : NeZero (card α)

theorem Fintype.card_le_one_iff {α : Type u_1} [Fintype α] : card α ≤ 1 ↔ ∀ (a b : α), a = b

theorem Fintype.card_le_one_iff_subsingleton {α : Type u_1} [Fintype α] : card α ≤ 1 ↔ Subsingleton α

theorem Fintype.one_lt_card_iff_nontrivial {α : Type u_1} [Fintype α] : 1 < card α ↔ Nontrivial α

theorem Fintype.exists_ne_of_one_lt_card {α : Type u_1} [Fintype α] (h : 1 < card α) (a : α) : ∃ (b : α), b ≠ a

theorem Fintype.exists_pair_of_one_lt_card {α : Type u_1} [Fintype α] (h : 1 < card α) : ∃ (a : α) (b : α), a ≠ b

theorem Fintype.card_eq_one_of_forall_eq {α : Type u_1} [Fintype α] {i : α} (h : ∀ (j : α), j = i) : card α = 1

theorem Fintype.one_lt_card {α : Type u_1} [Fintype α] [h : Nontrivial α] : 1 < card α

theorem Fintype.one_lt_card_iff {α : Type u_1} [Fintype α] : 1 < card α ↔ ∃ (a : α) (b : α), a ≠ b

theorem Fintype.bijective_iff_injective_and_card {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) : Function.Bijective f ↔ Function.Injective f ∧ card α = card β

theorem Fintype.bijective_iff_surjective_and_card {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) : Function.Bijective f ↔ Function.Surjective f ∧ card α = card β

theorem Function.LeftInverse.rightInverse_of_card_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : α → β} {g : β → α} (hfg : LeftInverse f g) (hcard : Fintype.card α ≤ Fintype.card β) : RightInverse f g

theorem Function.RightInverse.leftInverse_of_card_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : α → β} {g : β → α} (hfg : RightInverse f g) (hcard : Fintype.card β ≤ Fintype.card α) : LeftInverse f g

def Equiv.ofLeftInverseOfCardLE {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hβα : Fintype.card β ≤ Fintype.card α) (f : α → β) (g : β → α) (h : Function.LeftInverse g f) : α ≃ β

Construct an equivalence from functions that are inverse to each other.

Equations

• Equiv.ofLeftInverseOfCardLE hβα f g h = { toFun := f, invFun := g, left_inv := h, right_inv := ⋯ }

@[simp]

theorem Equiv.ofLeftInverseOfCardLE_symm_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hβα : Fintype.card β ≤ Fintype.card α) (f : α → β) (g : β → α) (h : Function.LeftInverse g f) (a✝ : β) : (ofLeftInverseOfCardLE hβα f g h).symm a✝ = g a✝

@[simp]

theorem Equiv.ofLeftInverseOfCardLE_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hβα : Fintype.card β ≤ Fintype.card α) (f : α → β) (g : β → α) (h : Function.LeftInverse g f) (a✝ : α) : (ofLeftInverseOfCardLE hβα f g h) a✝ = f a✝

def Equiv.ofRightInverseOfCardLE {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hαβ : Fintype.card α ≤ Fintype.card β) (f : α → β) (g : β → α) (h : Function.RightInverse g f) : α ≃ β

Construct an equivalence from functions that are inverse to each other.

Equations

• Equiv.ofRightInverseOfCardLE hαβ f g h = { toFun := f, invFun := g, left_inv := ⋯, right_inv := h }

@[simp]

theorem Equiv.ofRightInverseOfCardLE_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hαβ : Fintype.card α ≤ Fintype.card β) (f : α → β) (g : β → α) (h : Function.RightInverse g f) (a✝ : α) : (ofRightInverseOfCardLE hαβ f g h) a✝ = f a✝

@[simp]

theorem Equiv.ofRightInverseOfCardLE_symm_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hαβ : Fintype.card α ≤ Fintype.card β) (f : α → β) (g : β → α) (h : Function.RightInverse g f) (a✝ : β) : (ofRightInverseOfCardLE hαβ f g h).symm a✝ = g a✝

noncomputable def Finset.equivFin {α : Type u_1} (s : Finset α) : { x : α // x ∈ s } ≃ Fin s.card

Noncomputable equivalence between a finset s coerced to a type and Fin #s.

Equations

• s.equivFin = Fintype.equivFinOfCardEq ⋯

noncomputable def Finset.equivFinOfCardEq {α : Type u_1} {s : Finset α} {n : ℕ} (h : s.card = n) : { x : α // x ∈ s } ≃ Fin n

Noncomputable equivalence between a finset s as a fintype and Fin n, when there is a proof that #s = n.

Equations

• Finset.equivFinOfCardEq h = Fintype.equivFinOfCardEq ⋯

theorem Finset.card_eq_of_equiv_fin {α : Type u_1} {s : Finset α} {n : ℕ} (i : { x : α // x ∈ s } ≃ Fin n) : s.card = n

theorem Finset.card_eq_of_equiv_fintype {α : Type u_1} {β : Type u_2} {s : Finset α} [Fintype β] (i : { x : α // x ∈ s } ≃ β) : s.card = Fintype.card β

noncomputable def Finset.equivOfCardEq {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (h : s.card = t.card) : { x : α // x ∈ s } ≃ { x : β // x ∈ t }

Noncomputable equivalence between two finsets s and t as fintypes when there is a proof that #s = #t.

Equations

• Finset.equivOfCardEq h = Fintype.equivOfCardEq ⋯

theorem Finset.card_eq_of_equiv {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : { x : α // x ∈ s } ≃ { x : β // x ∈ t }) : s.card = t.card

noncomputable def Function.Embedding.equivOfFiniteSelfEmbedding {α : Type u_1} [Finite α] (e : α ↪ α) : α ≃ α

An embedding from a Fintype to itself can be promoted to an equivalence.

Equations

• e.equivOfFiniteSelfEmbedding = Equiv.ofBijective ⇑e ⋯

@[deprecated Function.Embedding.equivOfFiniteSelfEmbedding (since := "2024-12-05")]

def Function.Embedding.equivOfFintypeSelfEmbedding {α : Type u_1} [Finite α] (e : α ↪ α) : α ≃ α

Alias of Function.Embedding.equivOfFiniteSelfEmbedding.

---

An embedding from a Fintype to itself can be promoted to an equivalence.

Equations

• @Function.Embedding.equivOfFintypeSelfEmbedding = @Function.Embedding.equivOfFiniteSelfEmbedding

@[simp]

theorem Function.Embedding.toEmbedding_equivOfFiniteSelfEmbedding {α : Type u_1} [Finite α] (e : α ↪ α) : e.equivOfFiniteSelfEmbedding.toEmbedding = e

@[deprecated Function.Embedding.toEmbedding_equivOfFiniteSelfEmbedding (since := "2024-12-05")]

theorem Function.Embedding.equiv_of_fintype_self_embedding_to_embedding {α : Type u_1} [Finite α] (e : α ↪ α) : e.equivOfFiniteSelfEmbedding.toEmbedding = e

Alias of Function.Embedding.toEmbedding_equivOfFiniteSelfEmbedding.

noncomputable def Equiv.embeddingEquivOfFinite (α : Type u_4) [Finite α] : (α ↪ α) ≃ (α ≃ α)

On a finite type, equivalence between the self-embeddings and the bijections.

Equations

• Equiv.embeddingEquivOfFinite α = { toFun := fun (e : α ↪ α) => e.equivOfFiniteSelfEmbedding, invFun := fun (e : α ≃ α) => e.toEmbedding, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.embeddingEquivOfFinite_symm_apply (α : Type u_4) [Finite α] (e : α ≃ α) : (embeddingEquivOfFinite α).symm e = e.toEmbedding

@[simp]

theorem Equiv.embeddingEquivOfFinite_apply (α : Type u_4) [Finite α] (e : α ↪ α) : (embeddingEquivOfFinite α) e = e.equivOfFiniteSelfEmbedding

def Function.Embedding.truncOfCardLE {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (h : Fintype.card α ≤ Fintype.card β) : Trunc (α ↪ β)

A constructive embedding of a fintype α in another fintype β when card α ≤ card β.

Equations

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

theorem Function.Embedding.nonempty_of_card_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (h : Fintype.card α ≤ Fintype.card β) : Nonempty (α ↪ β)

theorem Function.Embedding.nonempty_iff_card_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] : Nonempty (α ↪ β) ↔ Fintype.card α ≤ Fintype.card β

theorem Function.Embedding.exists_of_card_le_finset {α : Type u_1} {β : Type u_2} [Fintype α] {s : Finset β} (h : Fintype.card α ≤ s.card) : ∃ (f : α ↪ β), Set.range ⇑f ⊆ ↑s

@[simp]

theorem Finset.univ_map_embedding {α : Type u_4} [Fintype α] (e : α ↪ α) : map e univ = univ

theorem Fintype.card_lt_of_surjective_not_injective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (h : Function.Surjective f) (h' : ¬Function.Injective f) : card β < card α

theorem Fintype.false {α : Type u_1} [Infinite α] (_h : Fintype α) : False

@[simp]

theorem isEmpty_fintype {α : Type u_4} : IsEmpty (Fintype α) ↔ Infinite α

noncomputable def fintypeOfNotInfinite {α : Type u_4} (h : ¬Infinite α) : Fintype α

A non-infinite type is a fintype.

Equations

• fintypeOfNotInfinite h = Fintype.ofFinite α

noncomputable def fintypeOrInfinite (α : Type u_4) : Fintype α ⊕' Infinite α

Any type is (classically) either a Fintype, or Infinite.

One can obtain the relevant typeclasses via cases fintypeOrInfinite α.

Equations

• fintypeOrInfinite α = if h : Infinite α then PSum.inr h else PSum.inl (fintypeOfNotInfinite h)

theorem Finset.exists_minimal {α : Type u_4} [Preorder α] (s : Finset α) (h : s.Nonempty) : ∃ m ∈ s, ∀ x ∈ s, ¬x < m

theorem Finset.exists_maximal {α : Type u_4} [Preorder α] (s : Finset α) (h : s.Nonempty) : ∃ m ∈ s, ∀ x ∈ s, ¬m < x

theorem Infinite.of_not_fintype {α : Type u_1} (h : Fintype α → False) : Infinite α

theorem Infinite.of_injective_to_set {α : Type u_1} {s : Set α} (hs : s ≠ Set.univ) {f : α → ↑s} (hf : Function.Injective f) : Infinite α

If s : Set α is a proper subset of α and f : α → s is injective, then α is infinite.

theorem Infinite.of_surjective_from_set {α : Type u_1} {s : Set α} (hs : s ≠ Set.univ) {f : ↑s → α} (hf : Function.Surjective f) : Infinite α

If s : Set α is a proper subset of α and f : s → α is surjective, then α is infinite.

theorem Infinite.exists_not_mem_finset {α : Type u_1} [Infinite α] (s : Finset α) : ∃ (x : α), x ∉ s

@[instance 100]

instance Infinite.instNontrivial (α : Type u_4) [Infinite α] : Nontrivial α

theorem Infinite.nonempty (α : Type u_4) [Infinite α] : Nonempty α

theorem Infinite.of_injective {α : Sort u_4} {β : Sort u_5} [Infinite β] (f : β → α) (hf : Function.Injective f) : Infinite α

theorem Infinite.of_surjective {α : Sort u_4} {β : Sort u_5} [Infinite β] (f : α → β) (hf : Function.Surjective f) : Infinite α

instance Infinite.instSigmaOfNonempty {α : Type u_1} {β : α → Type u_4} [Infinite α] [∀ (a : α), Nonempty (β a)] : Infinite ((a : α) × β a)

theorem Infinite.sigma_of_right {α : Type u_1} {β : α → Type u_4} {a : α} [Infinite (β a)] : Infinite ((a : α) × β a)

instance Infinite.instSigmaOfNonempty_1 {α : Type u_1} {β : α → Type u_4} [Nonempty α] [∀ (a : α), Infinite (β a)] : Infinite ((a : α) × β a)

instance instInfiniteNat : Infinite ℕ

instance Int.infinite : Infinite ℤ

instance instInfiniteMultisetOfNonempty {α : Type u_1} [Nonempty α] : Infinite (Multiset α)

instance instInfiniteListOfNonempty {α : Type u_1} [Nonempty α] : Infinite (List α)

instance String.infinite : Infinite String

instance Infinite.set {α : Type u_1} [Infinite α] : Infinite (Set α)

instance instInfiniteFinset {α : Type u_1} [Infinite α] : Infinite (Finset α)

instance instInfiniteOption {α : Type u_1} [Infinite α] : Infinite (Option α)

instance Sum.infinite_of_left {α : Type u_1} {β : Type u_2} [Infinite α] : Infinite (α ⊕ β)

instance Sum.infinite_of_right {α : Type u_1} {β : Type u_2} [Infinite β] : Infinite (α ⊕ β)

instance Prod.infinite_of_right {α : Type u_1} {β : Type u_2} [Nonempty α] [Infinite β] : Infinite (α × β)

instance Prod.infinite_of_left {α : Type u_1} {β : Type u_2} [Infinite α] [Nonempty β] : Infinite (α × β)

instance instInfiniteProdSubtypeCommute {α : Type u_1} [Mul α] [Infinite α] : Infinite { p : α × α // Commute p.1 p.2 }

noncomputable def Infinite.natEmbedding (α : Type u_4) [Infinite α] : ℕ ↪ α

Embedding of ℕ into an infinite type.

Equations

• Infinite.natEmbedding α = { toFun := Infinite.natEmbeddingAux✝ α, inj' := ⋯ }

theorem Infinite.exists_subset_card_eq (α : Type u_4) [Infinite α] (n : ℕ) : ∃ (s : Finset α), s.card = n

See Infinite.exists_superset_card_eq for a version that, for an s : Finset α, provides a superset t : Finset α, s ⊆ t such that #t is fixed.

theorem Infinite.exists_superset_card_eq {α : Type u_1} [Infinite α] (s : Finset α) (n : ℕ) (hn : s.card ≤ n) : ∃ (t : Finset α), s ⊆ t ∧ t.card = n

See Infinite.exists_subset_card_eq for a version that provides an arbitrary s : Finset α for any cardinality.

noncomputable def fintypeOfFinsetCardLe {ι : Type u_4} (n : ℕ) (w : ∀ (s : Finset ι), s.card ≤ n) : Fintype ι

If every finset in a type has bounded cardinality, that type is finite.

Equations

• fintypeOfFinsetCardLe n w = fintypeOfNotInfinite ⋯

theorem not_injective_infinite_finite {α : Sort u_4} {β : Sort u_5} [Infinite α] [Finite β] (f : α → β) : ¬Function.Injective f

instance Function.Embedding.is_empty {α : Sort u_4} {β : Sort u_5} [Infinite α] [Finite β] : IsEmpty (α ↪ β)

theorem not_surjective_finite_infinite {α : Sort u_4} {β : Sort u_5} [Finite α] [Infinite β] (f : α → β) : ¬Function.Surjective f

theorem List.exists_pw_disjoint_with_card {α : Type u_4} [Fintype α] {c : List ℕ} (hc : c.sum ≤ Fintype.card α) : ∃ (o : List (List α)), map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o

For any c : List ℕ whose sum is at most Fintype.card α, we can find o : List (List α) whose members have no duplicate, whose lengths given by c, and which are pairwise disjoint