doc-next-gen

Mathlib.Data.Finite.Card

Module docstring

{"# Cardinality of finite types

The cardinality of a finite type α is given by Nat.card α. This function has the \"junk value\" of 0 for infinite types, but to ensure the function has valid output, one just needs to know that it's possible to produce a Finite instance for the type. (Note: we could have defined a Finite.card that required you to supply a Finite instance, but (a) the function would be noncomputable anyway so there is no need to supply the instance and (b) the function would have a more complicated dependent type that easily leads to \"motive not type correct\" errors.)

Implementation notes

Theorems about Nat.card are sometimes incidentally true for both finite and infinite types. If removing a finiteness constraint results in no loss in legibility, we remove it. We generally put such theorems into the SetTheory.Cardinal.Finite module.

"}

Finite.equivFin definition
(α : Type*) [Finite α] : α ≃ Fin (Nat.card α)
Full source 
/-- There is (noncomputably) an equivalence between a finite type `α` and `Fin (Nat.card α)`. -/
def Finite.equivFin (α : Type*) [Finite α] : α ≃ Fin (Nat.card α) := by
  have := (Finite.exists_equiv_fin α).choose_spec.some
  rwa [Nat.card_eq_of_equiv_fin this]
Bijection between finite type and its cardinality-indexed finite ordinals
Informal description
For any finite type $\alpha$, there exists a bijection between $\alpha$ and the finite ordinal type $\mathrm{Fin}(n)$, where $n$ is the cardinality of $\alpha$ (i.e., $n = \text{Nat.card}\,\alpha$). This bijection is constructed noncomputably using the axiom of choice.
Finite.equivFinOfCardEq definition
[Finite α] {n : ℕ} (h : Nat.card α = n) : α ≃ Fin n
Full source 
/-- Similar to `Finite.equivFin` but with control over the term used for the cardinality. -/
def Finite.equivFinOfCardEq [Finite α] {n : ℕ} (h : Nat.card α = n) : α ≃ Fin n := by
  subst h
  apply Finite.equivFin
Bijection between finite type and finite ordinals of specified cardinality
Informal description
Given a finite type $\alpha$ and a natural number $n$ such that the cardinality of $\alpha$ is equal to $n$, there exists a bijection between $\alpha$ and the finite ordinal type $\mathrm{Fin}(n)$.
Nat.card_eq theorem
(α : Type*) : Nat.card α = if _ : Finite α then @Fintype.card α (Fintype.ofFinite α) else 0
Full source 
theorem Nat.card_eq (α : Type*) :
    Nat.card α = if _ : Finite α then @Fintype.card α (Fintype.ofFinite α) else 0 := by
  cases finite_or_infinite α
  · letI := Fintype.ofFinite α
    simp only [this, *, Nat.card_eq_fintype_card, dif_pos]
  · simp only [*, card_eq_zero_of_infinite, not_finite_iff_infinite.mpr, dite_false]
Cardinality Formula for Finite and Infinite Types: $\mathrm{Nat.card}\,\alpha = \mathrm{Fintype.card}\,\alpha$ if finite, $0$ otherwise
Informal description
For any type $\alpha$, the cardinality $\mathrm{Nat.card}\,\alpha$ is equal to the cardinality of $\alpha$ as a finite type (computed via `Fintype.card`) if $\alpha$ is finite, and $0$ otherwise. More precisely: \[ \mathrm{Nat.card}\,\alpha = \begin{cases} \mathrm{Fintype.card}\,\alpha & \text{if } \alpha \text{ is finite}, \\ 0 & \text{otherwise.} \end{cases} \]
Finite.card_pos_iff theorem
[Finite α] : 0 < Nat.card α ↔ Nonempty α
Full source 
theorem Finite.card_pos_iff [Finite α] : 0 < Nat.card α ↔ Nonempty α := by
  haveI := Fintype.ofFinite α
  rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
Positivity of Finite Cardinality Equivalent to Nonemptiness
Informal description
For a finite type $\alpha$, the cardinality $\mathrm{card}(\alpha)$ is positive if and only if $\alpha$ is nonempty. In other words, $0 < \mathrm{card}(\alpha) \leftrightarrow \text{Nonempty }\alpha$.
Finite.card_pos theorem
[Finite α] [h : Nonempty α] : 0 < Nat.card α
Full source 
theorem Finite.card_pos [Finite α] [h : Nonempty α] : 0 < Nat.card α :=
  Finite.card_pos_iff.mpr h
Positivity of Cardinality for Nonempty Finite Types
Informal description
For any nonempty finite type $\alpha$, the cardinality of $\alpha$ is positive, i.e., $0 < \mathrm{card}(\alpha)$.
Finite.card_eq theorem
[Finite α] [Finite β] : Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
Full source 
theorem card_eq [Finite α] [Finite β] : Nat.cardNat.card α = Nat.card β ↔ Nonempty (α ≃ β) := by
  haveI := Fintype.ofFinite α
  haveI := Fintype.ofFinite β
  simp only [Nat.card_eq_fintype_card, Fintype.card_eq]
Finite Types Have Equal Cardinality if and only if They Are in Bijection
Informal description
For finite types $\alpha$ and $\beta$, the cardinality of $\alpha$ equals the cardinality of $\beta$ if and only if there exists a bijection between $\alpha$ and $\beta$. In other words, $|\alpha| = |\beta| \leftrightarrow \text{Nonempty}(\alpha \simeq \beta)$.
Finite.card_le_one_iff_subsingleton theorem
[Finite α] : Nat.card α ≤ 1 ↔ Subsingleton α
Full source 
theorem card_le_one_iff_subsingleton [Finite α] : Nat.cardNat.card α ≤ 1 ↔ Subsingleton α := by
  haveI := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card, Fintype.card_le_one_iff_subsingleton]
Finite Cardinality at Most One iff Subsingleton
Informal description
For a finite type $\alpha$, the cardinality of $\alpha$ is at most 1 if and only if $\alpha$ is a subsingleton (i.e., all elements of $\alpha$ are equal).
Finite.one_lt_card_iff_nontrivial theorem
[Finite α] : 1 < Nat.card α ↔ Nontrivial α
Full source 
theorem one_lt_card_iff_nontrivial [Finite α] : 1 < Nat.card α ↔ Nontrivial α := by
  haveI := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card, Fintype.one_lt_card_iff_nontrivial]
Cardinality Greater Than One Characterizes Nontrivial Finite Types
Informal description
For any finite type $\alpha$, the cardinality of $\alpha$ is greater than $1$ if and only if $\alpha$ is a nontrivial type (i.e., it contains at least two distinct elements).
Finite.one_lt_card theorem
[Finite α] [h : Nontrivial α] : 1 < Nat.card α
Full source 
theorem one_lt_card [Finite α] [h : Nontrivial α] : 1 < Nat.card α :=
  one_lt_card_iff_nontrivial.mpr h
Cardinality of Nontrivial Finite Types Exceeds One
Informal description
For any finite and nontrivial type $\alpha$, the cardinality of $\alpha$ is greater than $1$, i.e., $|\alpha| > 1$.
Finite.card_option theorem
[Finite α] : Nat.card (Option α) = Nat.card α + 1
Full source 
@[simp]
theorem card_option [Finite α] : Nat.card (Option α) = Nat.card α + 1 := by
  haveI := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card, Fintype.card_option]
Cardinality of Option Type: $|\mathrm{Option}\ \alpha| = |\alpha| + 1$
Informal description
For any finite type $\alpha$, the cardinality of the type $\mathrm{Option}\ \alpha$ (formed by adjoining a new element to $\alpha$) is equal to the cardinality of $\alpha$ plus one, i.e., $|\mathrm{Option}\ \alpha| = |\alpha| + 1$.
Finite.card_le_of_injective theorem
[Finite β] (f : α → β) (hf : Function.Injective f) : Nat.card α ≤ Nat.card β
Full source 
theorem card_le_of_injective [Finite β] (f : α → β) (hf : Function.Injective f) :
    Nat.card α ≤ Nat.card β := by
  haveI := Fintype.ofFinite β
  haveI := Fintype.ofInjective f hf
  simpa only [Nat.card_eq_fintype_card] using Fintype.card_le_of_injective f hf
Cardinality Inequality for Injective Functions on Finite Types
Informal description
Let $\alpha$ and $\beta$ be types with $\beta$ finite. For any injective function $f \colon \alpha \to \beta$, the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$, i.e., $|\alpha| \leq |\beta|$.
Finite.card_le_of_embedding theorem
[Finite β] (f : α ↪ β) : Nat.card α ≤ Nat.card β
Full source 
theorem card_le_of_embedding [Finite β] (f : α ↪ β) : Nat.card α ≤ Nat.card β :=
  card_le_of_injective _ f.injective
Cardinality Inequality for Injective Embeddings on Finite Types
Informal description
Let $\alpha$ and $\beta$ be types with $\beta$ finite. For any injective function embedding $f \colon \alpha \hookrightarrow \beta$, the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$, i.e., $|\alpha| \leq |\beta|$.
Finite.card_le_of_surjective theorem
[Finite α] (f : α → β) (hf : Function.Surjective f) : Nat.card β ≤ Nat.card α
Full source 
theorem card_le_of_surjective [Finite α] (f : α → β) (hf : Function.Surjective f) :
    Nat.card β ≤ Nat.card α := by
  classical
  haveI := Fintype.ofFinite α
  haveI := Fintype.ofSurjective f hf
  simpa only [Nat.card_eq_fintype_card] using Fintype.card_le_of_surjective f hf
Cardinality Inequality for Surjective Functions on Finite Types
Informal description
Let $\alpha$ and $\beta$ be types with $\alpha$ finite. If $f : \alpha \to \beta$ is a surjective function, then the cardinality of $\beta$ is less than or equal to the cardinality of $\alpha$, i.e., $|\beta| \leq |\alpha|$.
Finite.card_eq_zero_iff theorem
[Finite α] : Nat.card α = 0 ↔ IsEmpty α
Full source 
theorem card_eq_zero_iff [Finite α] : Nat.cardNat.card α = 0 ↔ IsEmpty α := by
  haveI := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card, Fintype.card_eq_zero_iff]
Cardinality Zero Equivalence for Finite Types: $|\alpha| = 0 \leftrightarrow \alpha$ is empty
Informal description
For a finite type $\alpha$, the cardinality of $\alpha$ is zero if and only if $\alpha$ is empty. In other words, $|\alpha| = 0 \leftrightarrow \alpha$ has no elements.
Finite.card_le_of_injective' theorem
{f : α → β} (hf : Function.Injective f) (h : Nat.card β = 0 → Nat.card α = 0) : Nat.card α ≤ Nat.card β
Full source 
/-- If `f` is injective, then `Nat.card α ≤ Nat.card β`. We must also assume
  `Nat.card β = 0 → Nat.card α = 0` since `Nat.card` is defined to be `0` for infinite types. -/
theorem card_le_of_injective' {f : α → β} (hf : Function.Injective f)
    (h : Nat.card β = 0 → Nat.card α = 0) : Nat.card α ≤ Nat.card β :=
  (or_not_of_imp h).casesOn (fun h => le_of_eq_of_le h (Nat.zero_le _)) fun h =>
    @card_le_of_injective α β (Nat.finite_of_card_ne_zero h) f hf
Cardinality Inequality for Injective Functions: $|\alpha| \leq |\beta|$ when $f$ is injective and $|\beta|=0 \Rightarrow |\alpha|=0$
Informal description
Let $f \colon \alpha \to \beta$ be an injective function between types $\alpha$ and $\beta$. If the cardinality of $\beta$ is zero (i.e., $\beta$ is infinite or empty), then the cardinality of $\alpha$ must also be zero. Under these conditions, the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$, i.e., $|\alpha| \leq |\beta|$.
Finite.card_le_of_embedding' theorem
(f : α ↪ β) (h : Nat.card β = 0 → Nat.card α = 0) : Nat.card α ≤ Nat.card β
Full source 
/-- If `f` is an embedding, then `Nat.card α ≤ Nat.card β`. We must also assume
  `Nat.card β = 0 → Nat.card α = 0` since `Nat.card` is defined to be `0` for infinite types. -/
theorem card_le_of_embedding' (f : α ↪ β) (h : Nat.card β = 0 → Nat.card α = 0) :
    Nat.card α ≤ Nat.card β :=
  card_le_of_injective' f.2 h
Cardinality Inequality for Embeddings: $|\alpha| \leq |\beta|$ when $f$ is an embedding and $|\beta|=0 \Rightarrow |\alpha|=0$
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an embedding (injective function) between types $\alpha$ and $\beta$. If the cardinality of $\beta$ is zero (i.e., $\beta$ is infinite or empty), then the cardinality of $\alpha$ must also be zero. Under these conditions, the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$, i.e., $|\alpha| \leq |\beta|$.
Finite.card_le_of_surjective' theorem
{f : α → β} (hf : Function.Surjective f) (h : Nat.card α = 0 → Nat.card β = 0) : Nat.card β ≤ Nat.card α
Full source 
/-- If `f` is surjective, then `Nat.card β ≤ Nat.card α`. We must also assume
  `Nat.card α = 0 → Nat.card β = 0` since `Nat.card` is defined to be `0` for infinite types. -/
theorem card_le_of_surjective' {f : α → β} (hf : Function.Surjective f)
    (h : Nat.card α = 0 → Nat.card β = 0) : Nat.card β ≤ Nat.card α :=
  (or_not_of_imp h).casesOn (fun h => le_of_eq_of_le h (Nat.zero_le _)) fun h =>
    @card_le_of_surjective α β (Nat.finite_of_card_ne_zero h) f hf
Cardinality Inequality for Surjective Functions: $|\beta| \leq |\alpha|$ when $f$ is surjective and $|\alpha|=0 \Rightarrow |\beta|=0$
Informal description
Let $f \colon \alpha \to \beta$ be a surjective function between types $\alpha$ and $\beta$. If the cardinality of $\alpha$ is zero (i.e., $\alpha$ is infinite or empty), then the cardinality of $\beta$ must also be zero. Under these conditions, the cardinality of $\beta$ is less than or equal to the cardinality of $\alpha$, i.e., $|\beta| \leq |\alpha|$.
Finite.card_eq_zero_of_surjective theorem
{f : α → β} (hf : Function.Surjective f) (h : Nat.card β = 0) : Nat.card α = 0
Full source 
/-- NB: `Nat.card` is defined to be `0` for infinite types. -/
theorem card_eq_zero_of_surjective {f : α → β} (hf : Function.Surjective f) (h : Nat.card β = 0) :
    Nat.card α = 0 := by
  cases finite_or_infinite β
  · haveI := card_eq_zero_iff.mp h
    haveI := Function.isEmpty f
    exact Nat.card_of_isEmpty
  · haveI := Infinite.of_surjective f hf
    exact Nat.card_eq_zero_of_infinite
Surjective Function Preserves Zero Cardinality
Informal description
Let $f \colon \alpha \to \beta$ be a surjective function between types $\alpha$ and $\beta$. If the cardinality of $\beta$ is zero (i.e., $\beta$ is infinite or empty), then the cardinality of $\alpha$ must also be zero.
Finite.card_eq_zero_of_injective theorem
[Nonempty α] {f : α → β} (hf : Function.Injective f) (h : Nat.card α = 0) : Nat.card β = 0
Full source 
/-- NB: `Nat.card` is defined to be `0` for infinite types. -/
theorem card_eq_zero_of_injective [Nonempty α] {f : α → β} (hf : Function.Injective f)
    (h : Nat.card α = 0) : Nat.card β = 0 :=
  card_eq_zero_of_surjective (Function.invFun_surjective hf) h
Injective Function Preserves Infinite Cardinality
Informal description
Let $\alpha$ be a nonempty type and $f \colon \alpha \to \beta$ be an injective function. If the cardinality of $\alpha$ is zero (i.e., $\alpha$ is infinite), then the cardinality of $\beta$ must also be zero (i.e., $\beta$ is infinite).
Finite.card_eq_zero_of_embedding theorem
[Nonempty α] (f : α ↪ β) (h : Nat.card α = 0) : Nat.card β = 0
Full source 
/-- NB: `Nat.card` is defined to be `0` for infinite types. -/
theorem card_eq_zero_of_embedding [Nonempty α] (f : α ↪ β) (h : Nat.card α = 0) : Nat.card β = 0 :=
  card_eq_zero_of_injective f.2 h
Embedding Preserves Infinite Cardinality
Informal description
Let $\alpha$ be a nonempty type and $f \colon \alpha \hookrightarrow \beta$ be an embedding (injective function). If the cardinality of $\alpha$ is zero (i.e., $\alpha$ is infinite), then the cardinality of $\beta$ must also be zero (i.e., $\beta$ is infinite).
Finite.card_sum theorem
[Finite α] [Finite β] : Nat.card (α ⊕ β) = Nat.card α + Nat.card β
Full source 
theorem card_sum [Finite α] [Finite β] : Nat.card (α ⊕ β) = Nat.card α + Nat.card β := by
  haveI := Fintype.ofFinite α
  haveI := Fintype.ofFinite β
  simp only [Nat.card_eq_fintype_card, Fintype.card_sum]
Cardinality of Sum of Finite Types
Informal description
For any finite types $\alpha$ and $\beta$, the cardinality of their sum type $\alpha \oplus \beta$ is equal to the sum of their cardinalities, i.e., $|\alpha \oplus \beta| = |\alpha| + |\beta|$.
Finite.card_image_le theorem
{s : Set α} [Finite s] (f : α → β) : Nat.card (f '' s) ≤ Nat.card s
Full source 
theorem card_image_le {s : Set α} [Finite s] (f : α → β) : Nat.card (f '' s) ≤ Nat.card s :=
  card_le_of_surjective _ Set.surjective_onto_image
Cardinality Inequality for Images of Finite Sets: $|f(s)| \leq |s|$
Informal description
For any finite set $s \subseteq \alpha$ and any function $f : \alpha \to \beta$, the cardinality of the image $f(s)$ is less than or equal to the cardinality of $s$, i.e., $|f(s)| \leq |s|$.
Finite.card_range_le theorem
[Finite α] (f : α → β) : Nat.card (Set.range f) ≤ Nat.card α
Full source 
theorem card_range_le [Finite α] (f : α → β) : Nat.card (Set.range f) ≤ Nat.card α :=
  card_le_of_surjective _ Set.surjective_onto_range
Cardinality Inequality for Range of Function on Finite Type
Informal description
For any finite type $\alpha$ and any function $f : \alpha \to \beta$, the cardinality of the range of $f$ is less than or equal to the cardinality of $\alpha$, i.e., $|\mathrm{range}(f)| \leq |\alpha|$.
Finite.card_subtype_le theorem
[Finite α] (p : α → Prop) : Nat.card { x // p x } ≤ Nat.card α
Full source 
theorem card_subtype_le [Finite α] (p : α → Prop) : Nat.card { x // p x } ≤ Nat.card α := by
  classical
  haveI := Fintype.ofFinite α
  simpa only [Nat.card_eq_fintype_card] using Fintype.card_subtype_le p
Cardinality Bound for Subtypes of Finite Types
Informal description
For any finite type $\alpha$ and any predicate $p$ on $\alpha$, the cardinality of the subtype $\{x \in \alpha \mid p(x)\}$ is less than or equal to the cardinality of $\alpha$.
Finite.card_subtype_lt theorem
[Finite α] {p : α → Prop} {x : α} (hx : ¬p x) : Nat.card { x // p x } < Nat.card α
Full source 
theorem card_subtype_lt [Finite α] {p : α → Prop} {x : α} (hx : ¬p x) :
    Nat.card { x // p x } < Nat.card α := by
  classical
  haveI := Fintype.ofFinite α
  simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx
Cardinality of Proper Subtype is Strictly Less in Finite Types
Informal description
For any finite type $\alpha$ and any predicate $p$ on $\alpha$, if there exists an element $x \in \alpha$ such that $\neg p(x)$, then the cardinality of the subtype $\{x \in \alpha \mid p(x)\}$ is strictly less than the cardinality of $\alpha$.
ENat.card_eq_coe_natCard theorem
(α : Type*) [Finite α] : card α = Nat.card α
Full source 
theorem card_eq_coe_natCard (α : Type*) [Finite α] : card α = Nat.card α := by
  unfold ENat.card
  apply symm
  rw [Cardinal.natCast_eq_toENat_iff]
  exact Nat.cast_card
Equality of Extended and Finite Cardinalities for Finite Types
Informal description
For any finite type $\alpha$, the extended natural number cardinality of $\alpha$ is equal to the natural number cardinality of $\alpha$, i.e., $\mathrm{card}(\alpha) = \mathrm{Nat.card}(\alpha)$.
Set.card_union_le theorem
(s t : Set α) : Nat.card (↥(s ∪ t)) ≤ Nat.card s + Nat.card t
Full source 
theorem card_union_le (s t : Set α) : Nat.card (↥(s ∪ t)) ≤ Nat.card s + Nat.card t := by
  rcases _root_.finite_or_infinite (↥(s ∪ t)) with h | h
  · rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h
    cases h
    rw [← @Nat.cast_le Cardinal, Nat.cast_add, Nat.cast_card, Nat.cast_card, Nat.cast_card]
    exact Cardinal.mk_union_le s t
  · exact Nat.card_eq_zero_of_infinite.trans_le (zero_le _)
Cardinality Bound for Union of Sets: $\#(s \cup t) \leq \#s + \#t$
Informal description
For any two sets $s$ and $t$ in a type $\alpha$, the cardinality of their union satisfies the inequality $\#(s \cup t) \leq \#s + \#t$, where $\#$ denotes the cardinality of a set.
Set.Finite.card_lt_card theorem
(ht : t.Finite) (hsub : s ⊂ t) : Nat.card s < Nat.card t
Full source 
theorem card_lt_card (ht : t.Finite) (hsub : s ⊂ t) : Nat.card s < Nat.card t := by
  have : Fintype t := Finite.fintype ht
  have : Fintype s := Finite.fintype (subset ht (subset_of_ssubset hsub))
  simp only [Nat.card_eq_fintype_card]
  exact Set.card_lt_card hsub
Cardinality Strictly Decreases for Proper Subsets of Finite Sets
Informal description
For any finite set $t$ and any proper subset $s \subset t$, the cardinality of $s$ is strictly less than the cardinality of $t$.
Set.Finite.equiv_image_eq_iff_subset theorem
(e : α ≃ α) (hs : s.Finite) : e '' s = s ↔ e '' s ⊆ s
Full source 
theorem equiv_image_eq_iff_subset (e : α ≃ α) (hs : s.Finite) : e '' se '' s = s ↔ e '' s ⊆ s :=
  ⟨fun h ↦ by rw [h], fun h ↦ hs.eq_of_subset_of_card_le h <|
    ge_of_eq (Nat.card_congr (e.image s).symm)⟩
Image of Finite Set Under Equivalence Equals Set if and only if Image is Subset
Informal description
For a finite set $s$ in a type $\alpha$ and an equivalence $e : \alpha \simeq \alpha$, the image of $s$ under $e$ is equal to $s$ if and only if the image of $s$ under $e$ is a subset of $s$.