Cardinalities of finite types

Main declarations

• Fintype.card α: Cardinality of a fintype. Equal to Finset.univ.card.
• 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≃ fin n iff m = n.
• Infinite.natEmbedding: An embedding of ℕ into an infinite type.

We also provide the following versions of the pigeonholes principle.

• Fintype.exists_ne_map_eq_of_card_lt and isEpty_of_card_lt: Finitely many pigeons and pigeonholes. Weak formulation.
• Finite.exists_ne_map_eq_of_infinite: Infinitely many pigeons in finitely many pigeonholes. Weak formulation.
• Finite.exists_infinite_fiber: Infinitely many pigeons in finitely many pigeonholes. Strong formulation.

Some more pigeonhole-like statements can be found in Data.Fintype.CardEmbedding.

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: ℕ, ℤ
• type constructors: Multiset α, List α

ink

def Fintype.card (α : Type u_1) [inst : Fintype α] : ℕ

card α is the number of elements in α, defined when α is a fintype.

Equations

• Fintype.card α = Finset.card Finset.univ

ink

def Fintype.truncEquivFin (α : Type u_1) [inst : DecidableEq α] [inst : Fintype α] : Trunc (α ≃ Fin (Fintype.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≃ 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.

ink

noncomputable def Fintype.equivFin (α : Type u_1) [inst : Fintype α] : α ≃ Fin (Fintype.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≃ Fin n given Fintype.card α = n.

Equations

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

ink

def Fintype.truncFinBijection (α : Type u_1) [inst : Fintype α] : Trunc { f // 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.

ink

theorem Fintype.subtype_card {α : Type u_1} {p : α → Prop} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ p x) : Fintype.card { x // p x } = Finset.card s

ink

theorem Fintype.card_of_subtype {α : Type u_1} {p : α → Prop} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ p x) [inst : Fintype { x // p x }] : Fintype.card { x // p x } = Finset.card s

ink

@[simp]

theorem Fintype.card_ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) : Fintype.card ↑p = Finset.card s

ink

theorem Fintype.card_of_finset' {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) [inst : Fintype ↑p] : Fintype.card ↑p = Finset.card s

ink

theorem Fintype.ofEquiv_card {α : Type u_1} {β : Type u_2} [inst : Fintype α] (f : α ≃ β) : Fintype.card β = Fintype.card α

ink

theorem Fintype.card_congr {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (f : α ≃ β) : Fintype.card α = Fintype.card β

ink

theorem Fintype.card_congr' {α : Type u_1} {β : Type u_1} [inst : Fintype α] [inst : Fintype β] (h : α = β) : Fintype.card α = Fintype.card β

ink

def Fintype.truncEquivFinOfCardEq {α : Type u_1} [inst : Fintype α] [inst : DecidableEq α] {n : ℕ} (h : Fintype.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 α)≃ Fin (card α).

Equations

• Fintype.truncEquivFinOfCardEq h = Trunc.map (fun e => Equiv.trans e (Fin.cast h).toEquiv) (Fintype.truncEquivFin α)

ink

noncomputable def Fintype.equivFinOfCardEq {α : Type u_1} [inst : Fintype α] {n : ℕ} (h : Fintype.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 α)≃ Fin (card α).

Equations

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

ink

def Fintype.truncEquivOfCardEq {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] [inst : DecidableEq α] [inst : DecidableEq β] (h : Fintype.card α = Fintype.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

• Fintype.truncEquivOfCardEq h = Trunc.bind (Fintype.truncEquivFinOfCardEq h) fun e => Trunc.map (fun e' => Equiv.trans e (Equiv.symm e')) (Fintype.truncEquivFin β)

ink

noncomputable def Fintype.equivOfCardEq {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (h : Fintype.card α = Fintype.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 = Trunc.out (Fintype.truncEquivOfCardEq h)

ink

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

ink

@[simp]

theorem Fintype.card_ofSubsingleton {α : Type u_1} (a : α) [inst : Subsingleton α] : Fintype.card α = 1

Note: this lemma is specifically about Fintype.ofSubsingleton. For a statement about arbitrary Fintype instances, use either Fintype.card_le_one_iff_subsingleton or Fintype.card_unique.

ink

@[simp]

theorem Fintype.card_unique {α : Type u_1} [inst : Unique α] [h : Fintype α] : Fintype.card α = 1

ink

@[simp]

theorem Fintype.card_of_isEmpty {α : Type u_1} [inst : IsEmpty α] : Fintype.card α = 0

Note: this lemma is specifically about Fintype.of_is_empty. For a statement about arbitrary Fintype instances, use Fintype.card_eq_zero_iff.

ink

@[simp]

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

ink

theorem Finset.card_univ {α : Type u_1} [inst : Fintype α] : Finset.card Finset.univ = Fintype.card α

ink

theorem Finset.eq_univ_of_card {α : Type u_1} [inst : Fintype α] (s : Finset α) (hs : Finset.card s = Fintype.card α) : s = Finset.univ

ink

theorem Finset.card_eq_iff_eq_univ {α : Type u_1} [inst : Fintype α] (s : Finset α) : Finset.card s = Fintype.card α ↔ s = Finset.univ

ink

theorem Finset.card_le_univ {α : Type u_1} [inst : Fintype α] (s : Finset α) : Finset.card s ≤ Fintype.card α

ink

theorem Finset.card_lt_univ_of_not_mem {α : Type u_1} [inst : Fintype α] {s : Finset α} {x : α} (hx : ¬x ∈ s) : Finset.card s < Fintype.card α

ink

theorem Finset.card_lt_iff_ne_univ {α : Type u_1} [inst : Fintype α] (s : Finset α) : Finset.card s < Fintype.card α ↔ s ≠ Finset.univ

ink

theorem Finset.card_compl_lt_iff_nonempty {α : Type u_1} [inst : Fintype α] [inst : DecidableEq α] (s : Finset α) : Finset.card (sᶜ) < Fintype.card α ↔ Finset.Nonempty s

ink

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

ink

theorem Finset.card_compl {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (s : Finset α) : Finset.card (sᶜ) = Fintype.card α - Finset.card s

ink

theorem Fintype.card_compl_set {α : Type u_1} [inst : Fintype α] (s : Set α) [inst : Fintype ↑s] [inst : Fintype ↑(sᶜ)] : Fintype.card ↑(sᶜ) = Fintype.card α - Fintype.card ↑s

ink

@[simp]

theorem Fintype.card_fin (n : ℕ) : Fintype.card (Fin n) = n

ink

@[simp]

theorem Finset.card_fin (n : ℕ) : Finset.card Finset.univ = n

ink

theorem fin_injective : Function.Injective Fin

Fin as a map from ℕ to Type is injective. Note that since this is a statement about equality of types, using it should be avoided if possible.

ink

theorem Fin.cast_eq_cast' {n : ℕ} {m : ℕ} (h : Fin n = Fin m) : cast h = ↑(RelIso.toRelEmbedding (Fin.cast (_ : n = m))).toEmbedding

A reversed version of Fin.cast_eq_cast that is easier to rewrite with.

ink

theorem card_finset_fin_le {n : ℕ} (s : Finset (Fin n)) : Finset.card s ≤ n

ink

theorem Fin.equiv_iff_eq {m : ℕ} {n : ℕ} : Nonempty (Fin m ≃ Fin n) ↔ m = n

ink

theorem Fintype.card_subtype_eq {α : Type u_1} (y : α) [inst : Fintype { x // x = y }] : Fintype.card { x // x = y } = 1

ink

theorem Fintype.card_subtype_eq' {α : Type u_1} (y : α) [inst : Fintype { x // y = x }] : Fintype.card { x // y = x } = 1

ink

@[simp]

theorem Fintype.card_empty : Fintype.card Empty = 0

ink

@[simp]

theorem Fintype.card_pempty : Fintype.card PEmpty = 0

ink

theorem Fintype.card_unit : Fintype.card Unit = 1

ink

@[simp]

theorem Fintype.card_punit : Fintype.card PUnit = 1

ink

@[simp]

theorem Fintype.card_bool : Fintype.card Bool = 2

ink

@[simp]

theorem Fintype.card_ulift (α : Type u_1) [inst : Fintype α] : Fintype.card (ULift α) = Fintype.card α

ink

@[simp]

theorem Fintype.card_plift (α : Type u_1) [inst : Fintype α] : Fintype.card (PLift α) = Fintype.card α

ink

@[simp]

theorem Fintype.card_orderDual (α : Type u_1) [inst : Fintype α] : Fintype.card αᵒᵈ = Fintype.card α

ink

@[simp]

theorem Fintype.card_lex (α : Type u_1) [inst : Fintype α] : Fintype.card (Lex α) = Fintype.card α

ink

noncomputable def Fintype.sumLeft {α : Type u_1} {β : Type u_2} [inst : Fintype (α ⊕ β)] : Fintype α

Given that α ⊕ β⊕ β is a fintype, α is also a fintype. This is non-computable as it uses that Sum.inl is an injection, but there's no clear inverse if α is empty.

Equations

• Fintype.sumLeft = Fintype.ofInjective Sum.inl (_ : Function.Injective Sum.inl)

ink

noncomputable def Fintype.sumRight {α : Type u_1} {β : Type u_2} [inst : Fintype (α ⊕ β)] : Fintype β

Given that α ⊕ β⊕ β is a fintype, β is also a fintype. This is non-computable as it uses that Sum.inr is an injection, but there's no clear inverse if β is empty.

Equations

• Fintype.sumRight = Fintype.ofInjective Sum.inr (_ : Function.Injective Sum.inr)

Relation to Finite

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

ink

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

ink

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

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

Equations

• Finite.of_fintype = Finite.of_fintype.proof_1

ink

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

ink

theorem nonempty_fintype (α : Type u_1) [inst : Finite α] : Nonempty (Fintype α)

See also nonempty_encodable, nonempty_denumerable.

ink

noncomputable def Fintype.ofFinite (α : Type u_1) [inst : 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 α = Nonempty.some (_ : Nonempty (Fintype α))

ink

theorem Finite.of_injective {α : Sort u_1} {β : Sort u_2} [inst : Finite β] (f : α → β) (H : Function.Injective f) : Finite α

ink

theorem Finite.of_surjective {α : Sort u_1} {β : Sort u_2} [inst : Finite α] (f : α → β) (H : Function.Surjective f) : Finite β

ink

theorem Finite.exists_univ_list (α : Type u_1) [inst : Finite α] : ∃ l, List.Nodup l ∧ ∀ (x : α), x ∈ l

ink

theorem List.Nodup.length_le_card {α : Type u_1} [inst : Fintype α] {l : List α} (h : List.Nodup l) : List.length l ≤ Fintype.card α

ink

theorem Fintype.card_le_of_injective {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (f : α → β) (hf : Function.Injective f) : Fintype.card α ≤ Fintype.card β

ink

theorem Fintype.card_le_of_embedding {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (f : α ↪ β) : Fintype.card α ≤ Fintype.card β

ink

theorem Fintype.card_lt_of_injective_of_not_mem {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (f : α → β) (h : Function.Injective f) {b : β} (w : ¬b ∈ Set.range f) : Fintype.card α < Fintype.card β

ink

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

ink

theorem Fintype.card_le_of_surjective {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (f : α → β) (h : Function.Surjective f) : Fintype.card β ≤ Fintype.card α

ink

theorem Fintype.card_range_le {α : Type u_1} {β : Type u_2} (f : α → β) [inst : Fintype α] [inst : Fintype ↑(Set.range f)] : Fintype.card ↑(Set.range f) ≤ Fintype.card α

ink

theorem Fintype.card_range {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : EmbeddingLike F α β] (f : F) [inst : Fintype α] [inst : Fintype ↑(Set.range ↑f)] : Fintype.card ↑(Set.range ↑f) = Fintype.card α

ink

theorem Fintype.exists_ne_map_eq_of_card_lt {α : Type u_2} {β : Type u_1} [inst : Fintype α] [inst : Fintype β] (f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ x y, x ≠ y ∧ f x = f y

The pigeonhole principle for finitely many pigeons and pigeonholes. This is the Fintype version of Finset.exists_ne_map_eq_of_card_lt_of_maps_to.

ink

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

ink

theorem Fintype.card_eq_zero_iff {α : Type u_1} [inst : Fintype α] : Fintype.card α = 0 ↔ IsEmpty α

ink

theorem Fintype.card_eq_zero {α : Type u_1} [inst : Fintype α] [inst : IsEmpty α] : Fintype.card α = 0

ink

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

ink

def Fintype.cardEqZeroEquivEquivEmpty {α : Type u_1} [inst : Fintype α] : Fintype.card α = 0 ≃ (α ≃ Empty)

A Fintype with cardinality zero is equivalent to Empty.

Equations

• Fintype.cardEqZeroEquivEquivEmpty = Equiv.trans (Equiv.ofIff (_ : Fintype.card α = 0 ↔ IsEmpty α)) (Equiv.symm (Equiv.equivEmptyEquiv α))

ink

theorem Fintype.card_pos_iff {α : Type u_1} [inst : Fintype α] : 0 < Fintype.card α ↔ Nonempty α

ink

theorem Fintype.card_pos {α : Type u_1} [inst : Fintype α] [h : Nonempty α] : 0 < Fintype.card α

ink

theorem Fintype.card_ne_zero {α : Type u_1} [inst : Fintype α] [inst : Nonempty α] : Fintype.card α ≠ 0

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Fintype.two_lt_card_iff {α : Type u_1} [inst : Fintype α] : 2 < Fintype.card α ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c

ink

theorem Fintype.card_of_bijective {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] {f : α → β} (hf : Function.Bijective f) : Fintype.card α = Fintype.card β

ink

theorem Finite.surjective_of_injective {α : Type u_1} [inst : Finite α] {f : α → α} (hinj : Function.Injective f) : Function.Surjective f

ink

theorem Finite.injective_iff_surjective {α : Type u_1} [inst : Finite α] {f : α → α} : Function.Injective f ↔ Function.Surjective f

ink

theorem Finite.injective_iff_bijective {α : Type u_1} [inst : Finite α] {f : α → α} : Function.Injective f ↔ Function.Bijective f

ink

theorem Finite.surjective_iff_bijective {α : Type u_1} [inst : Finite α] {f : α → α} : Function.Surjective f ↔ Function.Bijective f

ink

theorem Finite.injective_iff_surjective_of_equiv {α : Type u_1} {β : Type u_2} [inst : Finite α] {f : α → β} (e : α ≃ β) : Function.Injective f ↔ Function.Surjective f

ink

theorem Function.Injective.bijective_of_finite {α : Type u_1} [inst : Finite α] {f : α → α} : Function.Injective f → Function.Bijective f

Alias of the forward direction of Finite.injective_iff_bijective.

ink

theorem Function.Surjective.bijective_of_finite {α : Type u_1} [inst : Finite α] {f : α → α} : Function.Surjective f → Function.Bijective f

Alias of the forward direction of Finite.surjective_iff_bijective.

ink

theorem Function.Surjective.injective_of_fintype {α : Type u_1} {β : Type u_2} [inst : Finite α] {f : α → β} (e : α ≃ β) : Function.Surjective f → Function.Injective f

Alias of the reverse direction of Finite.injective_iff_surjective_of_equiv.

ink

theorem Function.Injective.surjective_of_fintype {α : Type u_1} {β : Type u_2} [inst : Finite α] {f : α → β} (e : α ≃ β) : Function.Injective f → Function.Surjective f

Alias of the forward direction of Finite.injective_iff_surjective_of_equiv.

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

theorem Equiv.ofLeftInverseOfCardLe_apply {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (hβα : Fintype.card β ≤ Fintype.card α) (f : α → β) (g : β → α) (h : Function.LeftInverse g f) : ∀ (a : α), ↑(Equiv.ofLeftInverseOfCardLe hβα f g h) a = f a

ink

@[simp]

theorem Equiv.ofLeftInverseOfCardLe_symm_apply {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (hβα : Fintype.card β ≤ Fintype.card α) (f : α → β) (g : β → α) (h : Function.LeftInverse g f) : ∀ (a : β), ↑(Equiv.symm (Equiv.ofLeftInverseOfCardLe hβα f g h)) a = g a

ink

def Equiv.ofLeftInverseOfCardLe {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : 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 := (_ : Function.RightInverse g f) }

ink

@[simp]

theorem Equiv.ofRightInverseOfCardLe_apply {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (hαβ : Fintype.card α ≤ Fintype.card β) (f : α → β) (g : β → α) (h : Function.RightInverse g f) : ∀ (a : α), ↑(Equiv.ofRightInverseOfCardLe hαβ f g h) a = f a

ink

@[simp]

theorem Equiv.ofRightInverseOfCardLe_symm_apply {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (hαβ : Fintype.card α ≤ Fintype.card β) (f : α → β) (g : β → α) (h : Function.RightInverse g f) : ∀ (a : β), ↑(Equiv.symm (Equiv.ofRightInverseOfCardLe hαβ f g h)) a = g a

ink

def Equiv.ofRightInverseOfCardLe {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : 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 := (_ : Function.LeftInverse g f), right_inv := h }

ink

@[simp]

theorem Fintype.card_coe {α : Type u_1} (s : Finset α) [inst : Fintype { x // x ∈ s }] : Fintype.card { x // x ∈ s } = Finset.card s

ink

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

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

Equations

• Finset.equivFin s = Fintype.equivFinOfCardEq (_ : Fintype.card { x // x ∈ s } = Finset.card s)

ink

noncomputable def Finset.equivFinOfCardEq {α : Type u_1} {s : Finset α} {n : ℕ} (h : Finset.card s = 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.card = n.

Equations

• Finset.equivFinOfCardEq h = Fintype.equivFinOfCardEq (_ : Fintype.card { x // x ∈ s } = n)

ink

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

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

Equations

• Finset.equivOfCardEq h = Fintype.equivOfCardEq (_ : Fintype.card { x // x ∈ s } = Fintype.card { x // x ∈ t })

ink

@[simp]

theorem Fintype.card_Prop : Fintype.card Prop = 2

ink

theorem set_fintype_card_le_univ {α : Type u_1} [inst : Fintype α] (s : Set α) [inst : Fintype ↑s] : Fintype.card ↑s ≤ Fintype.card α

ink

theorem set_fintype_card_eq_univ_iff {α : Type u_1} [inst : Fintype α] (s : Set α) [inst : Fintype ↑s] : Fintype.card ↑s = Fintype.card α ↔ s = Set.univ

ink

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

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

Equations

• Function.Embedding.equivOfFintypeSelfEmbedding e = Equiv.ofBijective ↑e (_ : Function.Bijective e.toFun)

ink

@[simp]

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

ink

@[simp]

theorem Function.Embedding.is_empty_of_card_lt {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] (h : Fintype.card β < Fintype.card α) : IsEmpty (α ↪ β)

If ‖β‖ < ‖α‖ there are no embeddings α ↪ β↪ β. This is a formulation of the pigeonhole principle.

Note this cannot be an instance as it needs h.

ink

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

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

Equations

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

theorem Fintype.card_subtype_le {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst : DecidablePred p] : Fintype.card { x // p x } ≤ Fintype.card α

ink

theorem Fintype.card_subtype_lt {α : Type u_1} [inst : Fintype α] {p : α → Prop} [inst : DecidablePred p] {x : α} (hx : ¬p x) : Fintype.card { x // p x } < Fintype.card α

ink

theorem Fintype.card_subtype {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst : DecidablePred p] : Fintype.card { x // p x } = Finset.card (Finset.filter p Finset.univ)

ink

@[simp]

theorem Fintype.card_subtype_compl {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst : Fintype { x // p x }] [inst : Fintype { x // ¬p x }] : Fintype.card { x // ¬p x } = Fintype.card α - Fintype.card { x // p x }

ink

theorem Fintype.card_subtype_mono {α : Type u_1} (p : α → Prop) (q : α → Prop) (h : p ≤ q) [inst : Fintype { x // p x }] [inst : Fintype { x // q x }] : Fintype.card { x // p x } ≤ Fintype.card { x // q x }

ink

theorem Fintype.card_compl_eq_card_compl {α : Type u_1} [inst : Finite α] (p : α → Prop) (q : α → Prop) [inst : Fintype { x // p x }] [inst : Fintype { x // ¬p x }] [inst : Fintype { x // q x }] [inst : Fintype { x // ¬q x }] (h : Fintype.card { x // p x } = Fintype.card { x // q x }) : Fintype.card { x // ¬p x } = Fintype.card { x // ¬q x }

If two subtypes of a fintype have equal cardinality, so do their complements.

ink

theorem Fintype.card_quotient_le {α : Type u_1} [inst : Fintype α] (s : Setoid α) [inst : DecidableRel fun x x_1 => x ≈ x_1] : Fintype.card (Quotient s) ≤ Fintype.card α

ink

theorem Fintype.card_quotient_lt {α : Type u_1} [inst : Fintype α] {s : Setoid α} [inst : DecidableRel fun x x_1 => x ≈ x_1] {x : α} {y : α} (h1 : x ≠ y) (h2 : x ≈ y) : Fintype.card (Quotient s) < Fintype.card α

ink

theorem univ_eq_singleton_of_card_one {α : Type u_1} [inst : Fintype α] (x : α) (h : Fintype.card α = 1) : Finset.univ = {x}

ink

theorem Finite.wellFounded_of_trans_of_irrefl {α : Type u_1} [inst : Finite α] (r : α → α → Prop) [inst : IsTrans α r] [inst : IsIrrefl α r] : WellFounded r

ink

theorem Finite.Preorder.wellFounded_lt {α : Type u_1} [inst : Finite α] [inst : Preorder α] : WellFounded fun x x_1 => x < x_1

ink

theorem Finite.Preorder.wellFounded_gt {α : Type u_1} [inst : Finite α] [inst : Preorder α] : WellFounded fun x x_1 => x > x_1

ink

instance Finite.LinearOrder.isWellOrder_lt {α : Type u_1} [inst : Finite α] [inst : LinearOrder α] : IsWellOrder α fun x x_1 => x < x_1

Equations

• @Finite.LinearOrder.isWellOrder_lt = @Finite.LinearOrder.isWellOrder_lt.proof_1

ink

instance Finite.LinearOrder.isWellOrder_gt {α : Type u_1} [inst : Finite α] [inst : LinearOrder α] : IsWellOrder α fun x x_1 => x > x_1

Equations

• @Finite.LinearOrder.isWellOrder_gt = @Finite.LinearOrder.isWellOrder_gt.proof_1

ink

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

ink

@[simp]

theorem is_empty_fintype {α : Type u_1} : IsEmpty (Fintype α) ↔ Infinite α

ink

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

A non-infinite type is a fintype.

Equations

• fintypeOfNotInfinite h = Fintype.ofFinite α

ink

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

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

One can obtain the relevant typeclasses via cases fintype_or_infinite α; resetI.

Equations

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

ink

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

ink

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

ink

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

ink

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→ s is injective, then α is infinite.

ink

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.

ink

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

ink

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

Equations

• Infinite.instNontrivial = Infinite.instNontrivial.proof_1

ink

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

ink

theorem Infinite.of_injective {α : Sort u_1} {β : Sort u_2} [inst : Infinite β] (f : β → α) (hf : Function.Injective f) : Infinite α

ink

theorem Infinite.of_surjective {α : Sort u_1} {β : Sort u_2} [inst : Infinite β] (f : α → β) (hf : Function.Surjective f) : Infinite α

ink

instance instInfiniteNat : Infinite ℕ

Equations

• instInfiniteNat = instInfiniteNat.proof_1

ink

instance Int.infinite : Infinite ℤ

Equations

• Int.infinite = Int.infinite.proof_1

ink

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

Equations

• @instInfiniteMultiset = @instInfiniteMultiset.proof_1

ink

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

Equations

• @instInfiniteList = @instInfiniteList.proof_1

ink

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

Equations

• @Infinite.set = @Infinite.set.proof_1

ink

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

Equations

• @instInfiniteFinset = @instInfiniteFinset.proof_1

ink

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

Equations

• @instInfiniteOption = @instInfiniteOption.proof_1

ink

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

Equations

• @Sum.infinite_of_left = @Sum.infinite_of_left.proof_1

ink

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

Equations

• @Sum.infinite_of_right = @Sum.infinite_of_right.proof_1

ink

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

Equations

• @Prod.infinite_of_right = @Prod.infinite_of_right.proof_1

ink

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

Equations

• @Prod.infinite_of_left = @Prod.infinite_of_left.proof_1

ink

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

Embedding of ℕ into an infinite type.

Equations

• Infinite.natEmbedding α = { toFun := Infinite.natEmbeddingAux α, inj' := (_ : Function.Injective (Infinite.natEmbeddingAux α)) }

ink

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

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

ink

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

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

ink

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

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

Equations

• fintypeOfFinsetCardLe n w = fintypeOfNotInfinite (_ : Infinite ι → False)

ink

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

ink

theorem Finite.exists_ne_map_eq_of_infinite {α : Sort u_1} {β : Sort u_2} [inst : Infinite α] [inst : Finite β] (f : α → β) : ∃ x y, x ≠ y ∧ f x = f y

The pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are infinitely many pigeons in finitely many pigeonholes, then there are at least two pigeons in the same pigeonhole.

See also: Fintype.exists_ne_map_eq_of_card_lt, Finite.exists_infinite_fiber.

ink

instance Function.Embedding.is_empty {α : Sort u_1} {β : Sort u_2} [inst : Infinite α] [inst : Finite β] : IsEmpty (α ↪ β)

Equations

• @Function.Embedding.is_empty = @Function.Embedding.is_empty.proof_1

ink

theorem Finite.exists_infinite_fiber {α : Type u_1} {β : Type u_2} [inst : Infinite α] [inst : Finite β] (f : α → β) : ∃ y, Infinite ↑(f ⁻¹' {y})

The strong pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are infinitely many pigeons in finitely many pigeonholes, then there is a pigeonhole with infinitely many pigeons.

See also: Finite.exists_ne_map_eq_of_infinite

ink

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

ink

def truncOfCardPos {α : Type u_1} [inst : Fintype α] (h : 0 < Fintype.card α) : Trunc α

A Fintype with positive cardinality constructively contains an element.

Equations

• truncOfCardPos h = truncOfNonemptyFintype α

ink

theorem Fintype.induction_subsingleton_or_nontrivial {P : (α : Type u_1) → [inst : Fintype α] → Prop} (α : Type u_1) [inst : Fintype α] (hbase : (α : Type u_1) → [inst : Fintype α] → [inst_1 : Subsingleton α] → P α inst) (hstep : (α : Type u_1) → [inst : Fintype α] → [inst_1 : Nontrivial α] → ((β : Type u_1) → [inst_2 : Fintype β] → Fintype.card β < Fintype.card α → P β inst_2) → P α inst) : P α inst

A custom induction principle for fintypes. The base case is a subsingleton type, and the induction step is for non-trivial types, and one can assume the hypothesis for smaller types (via Fintype.card).

The major premise is Fintype α, so to use this with the induction tactic you have to give a name to that instance and use that name.