Mathlib.SetTheory.Cardinal.Finite

Nat.card definition

(α : Type*) : ℕ

Full source

/-- `Nat.card α` is the cardinality of `α` as a natural number.
  If `α` is infinite, `Nat.card α = 0`. -/
protected def card (α : Type*) : ℕ :=
  toNat (mk α)

Cardinality of a type as a natural number

Informal description

The function `Nat.card α` maps a type `α` to its cardinality as a natural number. If `α` is infinite, it returns 0. For finite types, it returns the number of elements in `α`, equivalent to the cardinality defined via `Fintype.card α`.

Nat.card_eq_fintype_card theorem

[Fintype α] : Nat.card α = Fintype.card α

Full source

@[simp]
theorem card_eq_fintype_card [Fintype α] : Nat.card α = Fintype.card α :=
  mk_toNat_eq_card

Equality of Natural Cardinality and Finite Type Cardinality

Informal description

For any finite type $\alpha$, the cardinality of $\alpha$ as a natural number equals the cardinality of $\alpha$ as a finite type, i.e., $\mathrm{Nat.card}(\alpha) = \mathrm{Fintype.card}(\alpha)$.

Fintype.card_eq_nat_card theorem

{_ : Fintype α} : Fintype.card α = Nat.card α

Full source

/-- Because this theorem takes `Fintype α` as a non-instance argument, it can be used in particular
when `Fintype.card` ends up with different instance than the one found by inference -/
theorem _root_.Fintype.card_eq_nat_card {_ : Fintype α} : Fintype.card α = Nat.card α :=
  mk_toNat_eq_card.symm

Equality of Finite Type Cardinality and Natural Number Cardinality

Informal description

For any finite type $\alpha$, the cardinality of $\alpha$ as a finite type is equal to the cardinality of $\alpha$ as a natural number, i.e., $\mathrm{card}(\alpha) = \mathrm{Nat.card}(\alpha)$.

Nat.card_eq_finsetCard theorem

(s : Finset α) : Nat.card s = s.card

Full source

lemma card_eq_finsetCard (s : Finset α) : Nat.card s = s.card := by
  simp only [Nat.card_eq_fintype_card, Fintype.card_coe]

Equality of Natural Cardinality and Finset Cardinality: $\mathrm{Nat.card}\, s = s.\mathrm{card}$

Informal description

For any finite set $s$ represented as a `Finset` of type $\alpha$, the cardinality of $s$ as a natural number (`Nat.card s`) is equal to the cardinality of $s$ as a finite set (`s.card`), i.e., $\mathrm{Nat.card}\, s = s.\mathrm{card}$.

Nat.card_eq_card_toFinset theorem

(s : Set α) [Fintype s] : Nat.card s = s.toFinset.card

Full source

lemma card_eq_card_toFinset (s : Set α) [Fintype s] : Nat.card s = s.toFinset.card := by
  simp only [← Nat.card_eq_finsetCard, s.mem_toFinset]

Equality of Cardinality for Finite Sets: $\mathrm{Nat.card}\, s = \mathrm{toFinset}\, s.\mathrm{card}$

Informal description

For any finite set $s$ of type $\alpha$, the cardinality of $s$ as a natural number (`Nat.card s`) is equal to the cardinality of the finite version of $s$ (`s.toFinset.card`).

Nat.card_eq_card_finite_toFinset theorem

{s : Set α} (hs : s.Finite) : Nat.card s = hs.toFinset.card

Full source

lemma card_eq_card_finite_toFinset {s : Set α} (hs : s.Finite) : Nat.card s = hs.toFinset.card := by
  simp only [← Nat.card_eq_finsetCard, hs.mem_toFinset]

Cardinality of Finite Set Equals Cardinality of Finset Representation

Informal description

For any finite set $s$ of type $\alpha$, the cardinality of $s$ as a natural number is equal to the cardinality of its finset representation, i.e., $\mathrm{Nat.card}\, s = |\mathrm{hs.toFinset}|$.

Nat.card_of_isEmpty theorem

[IsEmpty α] : Nat.card α = 0

Full source

@[simp] theorem card_of_isEmpty [IsEmpty α] : Nat.card α = 0 := by simp [Nat.card]

Cardinality of Empty Type is Zero (Natural Number Version)

Informal description

For any empty type $\alpha$, the natural number cardinality of $\alpha$ is zero, i.e., $\mathrm{Nat.card}(\alpha) = 0$.

Nat.card_eq_zero_of_infinite theorem

[Infinite α] : Nat.card α = 0

Full source

@[simp] lemma card_eq_zero_of_infinite [Infinite α] : Nat.card α = 0 := mk_toNat_of_infinite

Cardinality of Infinite Type is Zero: $\mathrm{Nat.card}(\alpha) = 0$

Informal description

For any infinite type $\alpha$, the natural number cardinality of $\alpha$ is zero, i.e., $\mathrm{Nat.card}(\alpha) = 0$.

Nat.cast_card theorem

[Finite α] : (Nat.card α : Cardinal) = Cardinal.mk α

Full source

lemma cast_card [Finite α] : (Nat.card α : Cardinal) = Cardinal.mk α := by
  rw [Nat.card, Cardinal.cast_toNat_of_lt_aleph0]
  exact Cardinal.lt_aleph0_of_finite _

Embedding of Finite Cardinality: $\mathrm{Nat.card}(\alpha) = \#\alpha$ for finite $\alpha$

Informal description

For any finite type $\alpha$, the canonical embedding of the natural number $\mathrm{Nat.card}(\alpha)$ (representing the cardinality of $\alpha$) into the cardinal numbers equals the cardinality of $\alpha$, i.e., $\mathrm{Nat.card}(\alpha) = \#\alpha$.

Set.Infinite.card_eq_zero theorem

{s : Set α} (hs : s.Infinite) : Nat.card s = 0

Full source

lemma _root_.Set.Infinite.card_eq_zero {s : Set α} (hs : s.Infinite) : Nat.card s = 0 :=
  @card_eq_zero_of_infinite _ hs.to_subtype

Zero Cardinality of Infinite Sets

Informal description

For any infinite set $s$ of type $\alpha$, the natural number cardinality of $s$ is zero, i.e., $\mathrm{Nat.card}(s) = 0$.

Nat.card_eq_zero theorem

: Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α

Full source

lemma card_eq_zero : Nat.cardNat.card α = 0 ↔ IsEmpty α ∨ Infinite α := by
  simp [Nat.card, mk_eq_zero_iff, aleph0_le_mk_iff]

Zero Cardinality Characterization for Empty or Infinite Types

Informal description

For any type $\alpha$, the natural number cardinality $\mathrm{Nat.card}\,\alpha$ is zero if and only if $\alpha$ is either empty or infinite. In other words, $\mathrm{Nat.card}\,\alpha = 0 \leftrightarrow \alpha \text{ is empty or infinite}$.

Nat.card_ne_zero theorem

: Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α

Full source

lemma card_ne_zero : Nat.cardNat.card α ≠ 0Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α := by simp [card_eq_zero, not_or]

Nonzero Cardinality Characterization for Finite Nonempty Types

Informal description

For any type $\alpha$, the cardinality $\mathrm{Nat.card}\,\alpha$ is nonzero if and only if $\alpha$ is nonempty and finite.

Nat.card_pos_iff theorem

: 0 < Nat.card α ↔ Nonempty α ∧ Finite α

Full source

lemma card_pos_iff : 0 < Nat.card α ↔ Nonempty α ∧ Finite α := by
  simp [Nat.card, mk_eq_zero_iff, mk_lt_aleph0_iff]

Positivity of Natural Cardinality Characterizes Nonempty Finite Types

Informal description

For any type $\alpha$, the cardinality $\mathrm{Nat.card}\,\alpha$ is positive if and only if $\alpha$ is nonempty and finite. In other words, $0 < \mathrm{Nat.card}\,\alpha \leftrightarrow \alpha \text{ is nonempty and finite}$.

Nat.card_pos theorem

[Nonempty α] [Finite α] : 0 < Nat.card α

Full source

@[simp] lemma card_pos [Nonempty α] [Finite α] : 0 < Nat.card α := card_pos_iff.2 ⟨‹_›, ‹_›⟩

Positivity of Cardinality for Nonempty Finite Types

Informal description

For any nonempty finite type $\alpha$, the cardinality $\mathrm{Nat.card}\,\alpha$ is strictly positive, i.e., $0 < \mathrm{Nat.card}\,\alpha$.

Nat.finite_of_card_ne_zero theorem

(h : Nat.card α ≠ 0) : Finite α

Full source

theorem finite_of_card_ne_zero (h : Nat.cardNat.card α ≠ 0) : Finite α := (card_ne_zero.1 h).2

Finite Type from Nonzero Cardinality

Informal description

For any type $\alpha$, if the natural number cardinality of $\alpha$ is nonzero, then $\alpha$ is finite.

Nat.card_congr theorem

(f : α ≃ β) : Nat.card α = Nat.card β

Full source

theorem card_congr (f : α ≃ β) : Nat.card α = Nat.card β :=
  Cardinal.toNat_congr f

Invariance of Finite Cardinality under Bijection

Informal description

For any types $\alpha$ and $\beta$ and a bijection $f : \alpha \simeq \beta$, the cardinalities of $\alpha$ and $\beta$ as natural numbers are equal, i.e., $\mathrm{Nat.card}(\alpha) = \mathrm{Nat.card}(\beta)$.

Nat.card_le_card_of_injective theorem

{α : Type u} {β : Type v} [Finite β] (f : α → β) (hf : Injective f) : Nat.card α ≤ Nat.card β

Full source

lemma card_le_card_of_injective {α : Type u} {β : Type v} [Finite β] (f : α → β)
    (hf : Injective f) : Nat.card α ≤ Nat.card β := by
  simpa using toNat_le_toNat (lift_mk_le_lift_mk_of_injective hf) (by simp [lt_aleph0_of_finite])

Cardinality Inequality for Injective Functions on Finite Types: $\mathrm{card}(\alpha) \leq \mathrm{card}(\beta)$

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ finite. For any injective function $f \colon \alpha \to \beta$, the cardinality of $\alpha$ as a natural number is less than or equal to the cardinality of $\beta$, i.e., $\mathrm{card}(\alpha) \leq \mathrm{card}(\beta)$.

Nat.card_le_card_of_surjective theorem

{α : Type u} {β : Type v} [Finite α] (f : α → β) (hf : Surjective f) : Nat.card β ≤ Nat.card α

Full source

lemma card_le_card_of_surjective {α : Type u} {β : Type v} [Finite α] (f : α → β)
    (hf : Surjective f) : Nat.card β ≤ Nat.card α := by
  have : lift.{u} #β ≤ lift.{v} #α := mk_le_of_surjective (ULift.map_surjective.2 hf)
  simpa using toNat_le_toNat this (by simp [lt_aleph0_of_finite])

Cardinality Comparison via Surjective Functions: $\mathrm{card}(\beta) \leq \mathrm{card}(\alpha)$ for Finite $\alpha$

Informal description

For any finite type $\alpha$ and any type $\beta$, if there exists a surjective function $f \colon \alpha \to \beta$, then the cardinality of $\beta$ (as a natural number) is less than or equal to the cardinality of $\alpha$, i.e., $\mathrm{card}(\beta) \leq \mathrm{card}(\alpha)$.

Nat.card_eq_of_bijective theorem

(f : α → β) (hf : Function.Bijective f) : Nat.card α = Nat.card β

Full source

theorem card_eq_of_bijective (f : α → β) (hf : Function.Bijective f) : Nat.card α = Nat.card β :=
  card_congr (Equiv.ofBijective f hf)

Equality of Finite Cardinalities under Bijection

Informal description

For any types $\alpha$ and $\beta$ and a bijective function $f \colon \alpha \to \beta$, the cardinalities of $\alpha$ and $\beta$ as natural numbers are equal, i.e., $\mathrm{Nat.card}(\alpha) = \mathrm{Nat.card}(\beta)$.

Nat.bijective_iff_injective_and_card theorem

[Finite β] (f : α → β) : Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β

Full source

protected theorem bijective_iff_injective_and_card [Finite β] (f : α → β) :
    BijectiveBijective f ↔ Injective f ∧ Nat.card α = Nat.card β := by
  rw [Bijective, and_congr_right_iff]
  intro h
  have := Fintype.ofFinite β
  have := Fintype.ofInjective f h
  revert h
  rw [← and_congr_right_iff, ← Bijective,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_injective_and_card]

Characterization of Bijections via Injectivity and Cardinality for Finite Codomains

Informal description

For a finite type $\beta$ and a function $f \colon \alpha \to \beta$, the function $f$ is bijective if and only if it is injective and the cardinality of $\alpha$ equals the cardinality of $\beta$ (as natural numbers), i.e., \[ \text{Bijective}(f) \leftrightarrow \text{Injective}(f) \land \mathrm{card}(\alpha) = \mathrm{card}(\beta). \]

Nat.bijective_iff_surjective_and_card theorem

[Finite α] (f : α → β) : Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β

Full source

protected theorem bijective_iff_surjective_and_card [Finite α] (f : α → β) :
    BijectiveBijective f ↔ Surjective f ∧ Nat.card α = Nat.card β := by
  classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]

Bijectivity Criterion for Finite Types: Surjectivity and Equal Cardinality

Informal description

For a finite type $\alpha$ and any function $f : \alpha \to \beta$, $f$ is bijective if and only if it is surjective and the cardinality of $\alpha$ (as a natural number) equals the cardinality of $\beta$.

Function.Injective.bijective_of_nat_card_le theorem

[Finite β] {f : α → β} (inj : Injective f) (hc : Nat.card β ≤ Nat.card α) : Bijective f

Full source

theorem _root_.Function.Injective.bijective_of_nat_card_le [Finite β] {f : α → β}
    (inj : Injective f) (hc : Nat.card β ≤ Nat.card α) : Bijective f :=
  (Nat.bijective_iff_injective_and_card f).mpr
    ⟨inj, hc.antisymm (card_le_card_of_injective f inj) |>.symm⟩

Bijectivity of Injective Functions under Cardinality Condition: $\mathrm{card}(\beta) \leq \mathrm{card}(\alpha)$ implies $f$ is bijective

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ finite. For any injective function $f \colon \alpha \to \beta$, if the cardinality of $\beta$ (as a natural number) is less than or equal to the cardinality of $\alpha$, then $f$ is bijective.

Function.Surjective.bijective_of_nat_card_le theorem

[Finite α] {f : α → β} (surj : Surjective f) (hc : Nat.card α ≤ Nat.card β) : Bijective f

Full source

theorem _root_.Function.Surjective.bijective_of_nat_card_le [Finite α] {f : α → β}
    (surj : Surjective f) (hc : Nat.card α ≤ Nat.card β) : Bijective f :=
  (Nat.bijective_iff_surjective_and_card f).mpr
    ⟨surj, hc.antisymm (card_le_card_of_surjective f surj)⟩

Bijectivity from Surjectivity and Cardinality Inequality: $\mathrm{card}(\alpha) \leq \mathrm{card}(\beta)$ Implies Bijectivity for Finite $\alpha$

Informal description

For any finite type $\alpha$ and any function $f \colon \alpha \to \beta$, if $f$ is surjective and the cardinality of $\alpha$ (as a natural number) is less than or equal to the cardinality of $\beta$, then $f$ is bijective.

Nat.card_eq_of_equiv_fin theorem

{α : Type*} {n : ℕ} (f : α ≃ Fin n) : Nat.card α = n

Full source

theorem card_eq_of_equiv_fin {α : Type*} {n : ℕ} (f : α ≃ Fin n) : Nat.card α = n := by
  simpa only [card_eq_fintype_card, Fintype.card_fin] using card_congr f

Cardinality via Bijection to Finite Ordinal: $\mathrm{Nat.card}(\alpha) = n$ when $\alpha \simeq \mathrm{Fin}(n)$

Informal description

For any type $\alpha$ and natural number $n$, if there exists a bijection $f : \alpha \simeq \mathrm{Fin}(n)$, then the cardinality of $\alpha$ as a natural number is equal to $n$, i.e., $\mathrm{Nat.card}(\alpha) = n$.

Nat.card_mono theorem

(ht : t.Finite) (h : s ⊆ t) : Nat.card s ≤ Nat.card t

Full source

lemma card_mono (ht : t.Finite) (h : s ⊆ t) : Nat.card s ≤ Nat.card t :=
  toNat_le_toNat (mk_le_mk_of_subset h) ht.lt_aleph0

Monotonicity of Finite Cardinality under Subset Inclusion

Informal description

For any sets $s$ and $t$ over a type $\alpha$, if $t$ is finite and $s$ is a subset of $t$ (i.e., $s \subseteq t$), then the cardinality of $s$ as a natural number is less than or equal to the cardinality of $t$, i.e., $\mathrm{card}(s) \leq \mathrm{card}(t)$.

Nat.card_image_le theorem

{f : α → β} (hs : s.Finite) : Nat.card (f '' s) ≤ Nat.card s

Full source

lemma card_image_le {f : α → β} (hs : s.Finite) : Nat.card (f '' s) ≤ Nat.card s :=
  have := hs.to_subtype; card_le_card_of_surjective (imageFactorization f s) surjective_onto_image

Cardinality Inequality for Images of Finite Sets: $\mathrm{card}(f(s)) \leq \mathrm{card}(s)$

Informal description

For any function $f \colon \alpha \to \beta$ and any finite set $s \subseteq \alpha$, the cardinality of the image $f(s)$ is less than or equal to the cardinality of $s$, i.e., $\mathrm{card}(f(s)) \leq \mathrm{card}(s)$.

Nat.card_image_of_injOn theorem

{f : α → β} (hf : s.InjOn f) : Nat.card (f '' s) = Nat.card s

Full source

lemma card_image_of_injOn {f : α → β} (hf : s.InjOn f) : Nat.card (f '' s) = Nat.card s := by
  classical
  obtain hs | hs := s.finite_or_infinite
  · have := hs.fintype
    have := fintypeImage s f
    simp_rw [Nat.card_eq_fintype_card, Set.card_image_of_inj_on hf]
  · have := hs.to_subtype
    have := (hs.image hf).to_subtype
    simp [Nat.card_eq_zero_of_infinite]

Cardinality Preservation under Injective Image: $\mathrm{card}(f(s)) = \mathrm{card}(s)$

Informal description

For any function $f : \alpha \to \beta$ that is injective on a set $s \subseteq \alpha$, the cardinality of the image $f(s)$ as a natural number equals the cardinality of $s$, i.e., $\mathrm{card}(f(s)) = \mathrm{card}(s)$. If $s$ is infinite, both cardinalities are zero.

Nat.card_image_of_injective theorem

{f : α → β} (hf : Injective f) (s : Set α) : Nat.card (f '' s) = Nat.card s

Full source

lemma card_image_of_injective {f : α → β} (hf : Injective f) (s : Set α) :
    Nat.card (f '' s) = Nat.card s := card_image_of_injOn hf.injOn

Cardinality Preservation under Injective Functions: $\mathrm{card}(f(s)) = \mathrm{card}(s)$

Informal description

For any injective function $f \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the cardinality of the image $f(s)$ as a natural number equals the cardinality of $s$, i.e., $\mathrm{card}(f(s)) = \mathrm{card}(s)$. If $s$ is infinite, both cardinalities are zero.

Nat.card_image_equiv theorem

(e : α ≃ β) : Nat.card (e '' s) = Nat.card s

Full source

lemma card_image_equiv (e : α ≃ β) : Nat.card (e '' s) = Nat.card s :=
    Nat.card_congr (e.image s).symm

Invariance of Finite Cardinality under Bijective Image

Informal description

For any equivalence (bijection) $e : \alpha \simeq \beta$ and any subset $s \subseteq \alpha$, the cardinality of the image $e(s) \subseteq \beta$ as a natural number is equal to the cardinality of $s$, i.e., $\mathrm{Nat.card}(e(s)) = \mathrm{Nat.card}(s)$. If $s$ is infinite, both sides evaluate to 0.

Nat.card_preimage_of_injOn theorem

{f : α → β} {s : Set β} (hf : (f ⁻¹' s).InjOn f) (hsf : s ⊆ range f) : Nat.card (f ⁻¹' s) = Nat.card s

Full source

lemma card_preimage_of_injOn {f : α → β} {s : Set β} (hf : (f ⁻¹' s).InjOn f) (hsf : s ⊆ range f) :
    Nat.card (f ⁻¹' s) = Nat.card s := by
  rw [← Nat.card_image_of_injOn hf, image_preimage_eq_iff.2 hsf]

Cardinality Preservation under Injective Preimage: $\mathrm{card}(f^{-1}(s)) = \mathrm{card}(s)$

Informal description

For any function $f : \alpha \to \beta$ and subset $s \subseteq \beta$ such that $f$ is injective on the preimage $f^{-1}(s)$ and $s$ is contained in the range of $f$, the cardinality of the preimage $f^{-1}(s)$ as a natural number equals the cardinality of $s$, i.e., $\mathrm{card}(f^{-1}(s)) = \mathrm{card}(s)$. If $s$ is infinite, both cardinalities are zero.

Nat.card_preimage_of_injective theorem

{f : α → β} {s : Set β} (hf : Injective f) (hsf : s ⊆ range f) : Nat.card (f ⁻¹' s) = Nat.card s

Full source

lemma card_preimage_of_injective {f : α → β} {s : Set β} (hf : Injective f) (hsf : s ⊆ range f) :
    Nat.card (f ⁻¹' s) = Nat.card s := card_preimage_of_injOn hf.injOn hsf

Cardinality Preservation under Injective Preimage: $\mathrm{card}(f^{-1}(s)) = \mathrm{card}(s)$

Informal description

For any injective function $f : \alpha \to \beta$ and any subset $s \subseteq \beta$ contained in the range of $f$, the cardinality of the preimage $f^{-1}(s)$ as a natural number equals the cardinality of $s$, i.e., $\mathrm{card}(f^{-1}(s)) = \mathrm{card}(s)$. If $s$ is infinite, both cardinalities are zero.

Nat.card_univ theorem

: Nat.card (univ : Set α) = Nat.card α

Full source

@[simp] lemma card_univ : Nat.card (univ : Set α) = Nat.card α :=
  card_congr (Equiv.Set.univ α)

Cardinality of Universal Set Equals Cardinality of Base Type

Informal description

The cardinality of the universal set on a type $\alpha$ (as a natural number) is equal to the cardinality of $\alpha$ itself, i.e., $\mathrm{Nat.card}(\mathrm{univ} : \mathrm{Set} \alpha) = \mathrm{Nat.card}(\alpha)$.

Nat.card_range_of_injective theorem

{f : α → β} (hf : Injective f) : Nat.card (range f) = Nat.card α

Full source

lemma card_range_of_injective {f : α → β} (hf : Injective f) :
    Nat.card (range f) = Nat.card α := by
  rw [← Nat.card_preimage_of_injective hf le_rfl]
  simp

Cardinality of Range Equals Cardinality of Domain for Injective Functions

Informal description

For any injective function $f : \alpha \to \beta$, the cardinality of the range of $f$ as a natural number equals the cardinality of $\alpha$, i.e., $\mathrm{card}(\mathrm{range}(f)) = \mathrm{card}(\alpha)$. If $\alpha$ is infinite, both cardinalities are zero.

Nat.equivFinOfCardPos definition

{α : Type*} (h : Nat.card α ≠ 0) : α ≃ Fin (Nat.card α)

Full source

/-- If the cardinality is positive, that means it is a finite type, so there is
an equivalence between `α` and `Fin (Nat.card α)`. See also `Finite.equivFin`. -/
def equivFinOfCardPos {α : Type*} (h : Nat.cardNat.card α ≠ 0) : α ≃ Fin (Nat.card α) := by
  cases fintypeOrInfinite α
  · simpa only [card_eq_fintype_card] using Fintype.equivFin α
  · simp only [card_eq_zero_of_infinite, ne_eq, not_true_eq_false] at h

Bijection between a finite type and its cardinality-indexed finite type

Informal description

For any type $\alpha$ with positive cardinality (i.e., finite), there exists a bijection between $\alpha$ and the finite type $\text{Fin}(n)$, where $n$ is the cardinality of $\alpha$ (i.e., $n = \text{Nat.card } \alpha$).

Nat.card_of_subsingleton theorem

(a : α) [Subsingleton α] : Nat.card α = 1

Full source

theorem card_of_subsingleton (a : α) [Subsingleton α] : Nat.card α = 1 := by
  letI := Fintype.ofSubsingleton a
  rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]

Cardinality of a Subsingleton is One

Informal description

For any type $\alpha$ that is a subsingleton (i.e., all elements are equal) and any element $a \in \alpha$, the cardinality of $\alpha$ as a natural number is $1$, i.e., $\mathrm{Nat.card}(\alpha) = 1$.

Nat.card_eq_one_iff_unique theorem

: Nat.card α = 1 ↔ Subsingleton α ∧ Nonempty α

Full source

theorem card_eq_one_iff_unique : Nat.cardNat.card α = 1 ↔ Subsingleton α ∧ Nonempty α :=
  Cardinal.toNat_eq_one_iff_unique

Characterization of Types with Cardinality One: $\mathrm{Nat.card}(\alpha) = 1 \leftrightarrow \text{Subsingleton } \alpha \land \text{Nonempty } \alpha$

Informal description

For any type $\alpha$, the natural number cardinality of $\alpha$ is equal to $1$ if and only if $\alpha$ is a subsingleton (has at most one element) and is nonempty (has at least one element). In other words, $\mathrm{Nat.card}(\alpha) = 1 \leftrightarrow \text{Subsingleton } \alpha \land \text{Nonempty } \alpha$.

Nat.card_unique theorem

[Nonempty α] [Subsingleton α] : Nat.card α = 1

Full source

@[simp]
theorem card_unique [Nonempty α] [Subsingleton α] : Nat.card α = 1 := by
  simp [card_eq_one_iff_unique, *]

Cardinality of a Nonempty Subsingleton is One

Informal description

For any nonempty type $\alpha$ that is a subsingleton (i.e., all elements are equal), the cardinality of $\alpha$ as a natural number is $1$.

Nat.card_eq_one_iff_exists theorem

: Nat.card α = 1 ↔ ∃ x : α, ∀ y : α, y = x

Full source

theorem card_eq_one_iff_exists : Nat.cardNat.card α = 1 ↔ ∃ x : α, ∀ y : α, y = x := by
  rw [card_eq_one_iff_unique]
  exact ⟨fun ⟨s, ⟨a⟩⟩ ↦ ⟨a, fun x ↦ s.elim x a⟩, fun ⟨x, h⟩ ↦ ⟨subsingleton_of_forall_eq x h, ⟨x⟩⟩⟩

Characterization of Singleton Types via Cardinality: $\mathrm{Nat.card}(\alpha) = 1 \leftrightarrow \exists! x \in \alpha$

Informal description

For any type $\alpha$, the natural number cardinality of $\alpha$ is equal to $1$ if and only if there exists an element $x \in \alpha$ such that every element $y \in \alpha$ is equal to $x$. In other words, $\mathrm{Nat.card}(\alpha) = 1 \leftrightarrow \exists x \in \alpha, \forall y \in \alpha, y = x$.

Nat.card_eq_two_iff theorem

: Nat.card α = 2 ↔ ∃ x y : α, x ≠ y ∧ { x, y } = @Set.univ α

Full source

theorem card_eq_two_iff : Nat.cardNat.card α = 2 ↔ ∃ x y : α, x ≠ y ∧ {x, y} = @Set.univ α :=
  toNat_eq_ofNat.trans mk_eq_two_iff

Characterization of Types with Cardinality 2: $\text{Nat.card}(\alpha) = 2 \leftrightarrow \exists x \neq y, \{x, y\} = \text{univ}$

Informal description

For any type $\alpha$, the natural number cardinality of $\alpha$ is equal to 2 if and only if there exist two distinct elements $x, y \in \alpha$ such that the set $\{x, y\}$ is equal to the universal set on $\alpha$.

Nat.card_eq_two_iff' theorem

(x : α) : Nat.card α = 2 ↔ ∃! y, y ≠ x

Full source

theorem card_eq_two_iff' (x : α) : Nat.cardNat.card α = 2 ↔ ∃! y, y ≠ x :=
  toNat_eq_ofNat.trans (mk_eq_two_iff' x)

Characterization of Types with Cardinality Two via Unique Distinct Element: $\mathrm{Nat.card}(\alpha) = 2 \leftrightarrow \exists! y \neq x$

Informal description

For any type $\alpha$ and any element $x \in \alpha$, the natural number cardinality of $\alpha$ is equal to 2 if and only if there exists a unique element $y \in \alpha$ such that $y \neq x$. In other words, $\mathrm{Nat.card}(\alpha) = 2 \leftrightarrow \exists! y \in \alpha, y \neq x$.

Nat.card_subtype_true theorem

: Nat.card { _a : α // True } = Nat.card α

Full source

@[simp]
theorem card_subtype_true : Nat.card {_a : α // True} = Nat.card α :=
  card_congr <| Equiv.subtypeUnivEquiv fun _ => trivial

Cardinality of Trivial Subtype Equals Original Type's Cardinality

Informal description

For any type $\alpha$, the cardinality of the subtype $\{a : \alpha \mid \text{True}\}$ is equal to the cardinality of $\alpha$ itself, i.e., $\mathrm{Nat.card}\{a : \alpha \mid \text{True}\} = \mathrm{Nat.card}(\alpha)$.

Nat.card_sum theorem

[Finite α] [Finite β] : Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Full source

@[simp]
theorem card_sum [Finite α] [Finite β] : Nat.card (α ⊕ β) = Nat.card α + Nat.card β := by
  have := Fintype.ofFinite α
  have := Fintype.ofFinite β
  simp_rw [Nat.card_eq_fintype_card, Fintype.card_sum]

Cardinality of Sum Type for Finite Types: $\mathrm{Nat.card}(\alpha \oplus \beta) = \mathrm{Nat.card}(\alpha) + \mathrm{Nat.card}(\beta)$

Informal description

For any finite types $\alpha$ and $\beta$, the cardinality of their sum type $\alpha \oplus \beta$ as a natural number is equal to the sum of the cardinalities of $\alpha$ and $\beta$, i.e., $\mathrm{Nat.card}(\alpha \oplus \beta) = \mathrm{Nat.card}(\alpha) + \mathrm{Nat.card}(\beta)$.

Nat.card_prod theorem

(α β : Type*) : Nat.card (α × β) = Nat.card α * Nat.card β

Full source

@[simp]
theorem card_prod (α β : Type*) : Nat.card (α × β) = Nat.card α * Nat.card β := by
  simp only [Nat.card, mk_prod, toNat_mul, toNat_lift]

Cardinality of Product Type: $\mathrm{Nat.card}(\alpha \times \beta) = \mathrm{Nat.card}(\alpha) \cdot \mathrm{Nat.card}(\beta)$

Informal description

For any types $\alpha$ and $\beta$, the cardinality of their product type $\alpha \times \beta$ as a natural number is equal to the product of the cardinalities of $\alpha$ and $\beta$, i.e., $\mathrm{Nat.card}(\alpha \times \beta) = \mathrm{Nat.card}(\alpha) \cdot \mathrm{Nat.card}(\beta)$. If either $\alpha$ or $\beta$ is infinite, the cardinality of the product is $0$.

Nat.card_ulift theorem

(α : Type*) : Nat.card (ULift α) = Nat.card α

Full source

@[simp]
theorem card_ulift (α : Type*) : Nat.card (ULift α) = Nat.card α :=
  card_congr Equiv.ulift

Cardinality Preservation under Lifting: $\mathrm{Nat.card}(\mathrm{ULift}\,\alpha) = \mathrm{Nat.card}(\alpha)$

Informal description

For any type $\alpha$, the cardinality of the lifted type $\mathrm{ULift}\,\alpha$ is equal to the cardinality of $\alpha$ when measured as natural numbers, i.e., $\mathrm{Nat.card}(\mathrm{ULift}\,\alpha) = \mathrm{Nat.card}(\alpha)$.

Nat.card_plift theorem

(α : Type*) : Nat.card (PLift α) = Nat.card α

Full source

@[simp]
theorem card_plift (α : Type*) : Nat.card (PLift α) = Nat.card α :=
  card_congr Equiv.plift

Cardinality Preservation under PLift: $\mathrm{Nat.card}(\mathrm{PLift}\,\alpha) = \mathrm{Nat.card}(\alpha)$

Informal description

For any type $\alpha$, the cardinality of the lifted type $\mathrm{PLift}\,\alpha$ is equal to the cardinality of $\alpha$ when measured as natural numbers, i.e., $\mathrm{Nat.card}(\mathrm{PLift}\,\alpha) = \mathrm{Nat.card}(\alpha)$.

Nat.card_sigma theorem

{β : α → Type*} [Fintype α] [∀ a, Finite (β a)] : Nat.card (Sigma β) = ∑ a, Nat.card (β a)

Full source

theorem card_sigma {β : α → Type*} [Fintype α] [∀ a, Finite (β a)] :
    Nat.card (Sigma β) = ∑ a, Nat.card (β a) := by
  letI _ (a : α) : Fintype (β a) := Fintype.ofFinite (β a)
  simp_rw [Nat.card_eq_fintype_card, Fintype.card_sigma]

Cardinality of Dependent Sum Equals Sum of Cardinalities for Finite Index Type

Informal description

For any finite type $\alpha$ and any family of types $\{\beta_a\}_{a \in \alpha}$ where each $\beta_a$ is finite, the cardinality of the dependent sum type $\Sigma_{a \in \alpha} \beta_a$ (as a natural number) is equal to the sum of the cardinalities of the individual types $\beta_a$. That is, \[ \mathrm{card}(\Sigma_{a \in \alpha} \beta_a) = \sum_{a \in \alpha} \mathrm{card}(\beta_a). \]

Nat.card_pi theorem

{β : α → Type*} [Fintype α] : Nat.card (∀ a, β a) = ∏ a, Nat.card (β a)

Full source

theorem card_pi {β : α → Type*} [Fintype α] : Nat.card (∀ a, β a) = ∏ a, Nat.card (β a) := by
  simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, map_prod]

Cardinality of Dependent Product Equals Product of Cardinalities for Finite Index Type

Informal description

For any finite type $\alpha$ and any family of types $\{\beta_a\}_{a \in \alpha}$, the cardinality of the dependent product type $\prod_{a \in \alpha} \beta_a$ (as a natural number) is equal to the product of the cardinalities of the individual types $\beta_a$. That is, \[ \mathrm{card}(\prod_{a \in \alpha} \beta_a) = \prod_{a \in \alpha} \mathrm{card}(\beta_a). \] If any $\beta_a$ is infinite, both sides evaluate to 0.

Nat.card_fun theorem

[Finite α] : Nat.card (α → β) = Nat.card β ^ Nat.card α

Full source

theorem card_fun [Finite α] : Nat.card (α → β) = Nat.card β ^ Nat.card α := by
  haveI := Fintype.ofFinite α
  rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]

Cardinality of Function Space as Exponentiation of Cardinalities for Finite Domain

Informal description

For any finite type $\alpha$ and any type $\beta$, the cardinality of the function type $\alpha \to \beta$ (as a natural number) is equal to the cardinality of $\beta$ raised to the power of the cardinality of $\alpha$. That is, \[ \mathrm{card}(\alpha \to \beta) = \mathrm{card}(\beta)^{\mathrm{card}(\alpha)}. \] If $\beta$ is infinite, both sides evaluate to 0.

Nat.card_zmod theorem

(n : ℕ) : Nat.card (ZMod n) = n

Full source

@[simp]
theorem card_zmod (n : ℕ) : Nat.card (ZMod n) = n := by
  cases n
  · exact @Nat.card_eq_zero_of_infinite _ Int.infinite
  · rw [Nat.card_eq_fintype_card, ZMod.card]

Cardinality of $\mathbb{Z}/n\mathbb{Z}$ is $n$

Informal description

For any natural number $n$, the cardinality of the ring $\mathbb{Z}/n\mathbb{Z}$ (as a natural number) is equal to $n$, i.e., $\mathrm{card}(\mathbb{Z}/n\mathbb{Z}) = n$.

Set.card_singleton_prod theorem

(a : α) (t : Set β) : Nat.card ({ a } ×ˢ t) = Nat.card t

Full source

lemma card_singleton_prod (a : α) (t : Set β) : Nat.card ({a} ×ˢ t) = Nat.card t := by
  rw [singleton_prod, Nat.card_image_of_injective (Prod.mk_right_injective a)]

Cardinality of Cartesian Product with Singleton: $\mathrm{card}(\{a\} \times t) = \mathrm{card}(t)$

Informal description

For any element $a$ in a type $\alpha$ and any subset $t \subseteq \beta$, the cardinality of the Cartesian product $\{a\} \times t$ as a natural number equals the cardinality of $t$, i.e., $\mathrm{card}(\{a\} \times t) = \mathrm{card}(t)$. If $t$ is infinite, both cardinalities are zero.

Set.natCard_pos theorem

(hs : s.Finite) : 0 < Nat.card s ↔ s.Nonempty

Full source

theorem natCard_pos (hs : s.Finite) : 0 < Nat.card s ↔ s.Nonempty := by
  simp [pos_iff_ne_zero, Nat.card_eq_zero, hs.to_subtype, nonempty_iff_ne_empty]

Positive Cardinality of Finite Set Equivalent to Nonemptiness

Informal description

For any finite set $s$ over a type $\alpha$, the cardinality of $s$ as a natural number is positive if and only if $s$ is nonempty. In other words, $0 < \text{Nat.card}(s) \leftrightarrow s.\text{Nonempty}$.

Set.natCard_graphOn theorem

(s : Set α) (f : α → β) : Nat.card (s.graphOn f) = Nat.card s

Full source

@[simp] lemma natCard_graphOn (s : Set α) (f : α → β) : Nat.card (s.graphOn f) = Nat.card s := by
  rw [← Nat.card_image_of_injOn fst_injOn_graph, image_fst_graphOn]

Cardinality of Graph Equals Cardinality of Domain

Informal description

For any set $s \subseteq \alpha$ and any function $f : \alpha \to \beta$, the cardinality of the graph of $f$ on $s$ (as a natural number) equals the cardinality of $s$ itself. That is, $$\mathrm{card}\big(\{(x, f(x)) \mid x \in s\}\big) = \mathrm{card}(s).$$ If $s$ is infinite, both cardinalities are zero.

ENat.card definition

(α : Type*) : ℕ∞

Full source

/-- `ENat.card α` is the cardinality of `α` as an extended natural number.
  If `α` is infinite, `ENat.card α = ⊤`. -/
def card (α : Type*) : ℕ∞ :=
  toENat (mk α)

Cardinality as an extended natural number

Informal description

The function maps a type $\alpha$ to its cardinality as an extended natural number $\mathbb{N}_\infty$. If $\alpha$ is finite, it returns the natural number corresponding to its cardinality; if $\alpha$ is infinite, it returns $\infty$.

ENat.card_eq_coe_fintype_card theorem

[Fintype α] : card α = Fintype.card α

Full source

@[simp]
theorem card_eq_coe_fintype_card [Fintype α] : card α = Fintype.card α := by
  simp [card]

Finite Type Cardinality as Extended Natural Number Equals Fintype Cardinality

Informal description

For any finite type $\alpha$ (i.e., $\alpha$ has a `Fintype` instance), the extended natural number cardinality of $\alpha$ is equal to the number of elements in $\alpha$ as given by `Fintype.card`. In other words, $\mathrm{card}(\alpha) = \mathrm{Fintype.card}(\alpha)$ when $\alpha$ is finite.

ENat.card_eq_top_of_infinite theorem

[Infinite α] : card α = ⊤

Full source

@[simp high]
theorem card_eq_top_of_infinite [Infinite α] : card α = ⊤ := by
  simp only [card, toENat_eq_top, aleph0_le_mk]

Infinite types have cardinality $\infty$ in extended natural numbers

Informal description

For any infinite type $\alpha$, the extended natural number cardinality of $\alpha$ is $\infty$.

ENat.card_eq_top theorem

: card α = ⊤ ↔ Infinite α

Full source

@[simp] lemma card_eq_top : cardcard α = ⊤ ↔ Infinite α := by simp [card, aleph0_le_mk_iff]

Extended Cardinality Equals Infinity iff Type is Infinite

Informal description

For any type $\alpha$, the extended natural number cardinality of $\alpha$ is $\infty$ if and only if $\alpha$ is infinite. In other words, $\mathrm{card}(\alpha) = \top \leftrightarrow \text{Infinite}(\alpha)$.

ENat.card_lt_top_of_finite theorem

[Finite α] : card α < ⊤

Full source

@[simp] theorem card_lt_top_of_finite [Finite α] : card α < ⊤ := by simp [card]

Finite types have cardinality less than infinity in $\mathbb{N}_\infty$

Informal description

For any finite type $\alpha$, the extended natural number cardinality of $\alpha$ is strictly less than $\infty$.

ENat.card_sum theorem

(α β : Type*) : card (α ⊕ β) = card α + card β

Full source

@[simp]
theorem card_sum (α β : Type*) :
    card (α ⊕ β) = card α + card β := by
  simp only [card, mk_sum, map_add, toENat_lift]

Cardinality of Sum Type in Extended Naturals

Informal description

For any types $\alpha$ and $\beta$, the extended natural number cardinality of their sum type $\alpha \oplus \beta$ is equal to the sum of their individual cardinalities, i.e., $$\mathrm{card}(\alpha \oplus \beta) = \mathrm{card}(\alpha) + \mathrm{card}(\beta).$$

ENat.card_congr theorem

{α β : Type*} (f : α ≃ β) : card α = card β

Full source

theorem card_congr {α β : Type*} (f : α ≃ β) : card α = card β :=
  Cardinal.toENat_congr f

Bijection Preserves Cardinality in Extended Naturals

Informal description

For any types $\alpha$ and $\beta$ with a bijection $f : \alpha \simeq \beta$, the extended natural number cardinalities of $\alpha$ and $\beta$ are equal, i.e., $\mathrm{card}(\alpha) = \mathrm{card}(\beta)$.

ENat.card_ulift theorem

(α : Type*) : card (ULift α) = card α

Full source

@[simp] lemma card_ulift (α : Type*) : card (ULift α) = card α := card_congr Equiv.ulift

Cardinality Preservation under Type Lifting ($\mathrm{ULift}$)

Informal description

For any type $\alpha$, the extended natural number cardinality of the lifted type $\mathrm{ULift}\,\alpha$ is equal to the cardinality of $\alpha$, i.e., $\mathrm{card}(\mathrm{ULift}\,\alpha) = \mathrm{card}(\alpha)$.

ENat.card_plift theorem

(α : Type*) : card (PLift α) = card α

Full source

@[simp] lemma card_plift (α : Type*) : card (PLift α) = card α := card_congr Equiv.plift

Cardinality Preservation under PLift: $\mathrm{card}(\mathrm{PLift}\,\alpha) = \mathrm{card}(\alpha)$

Informal description

For any type $\alpha$, the extended natural number cardinality of $\mathrm{PLift}\,\alpha$ is equal to the extended natural number cardinality of $\alpha$, i.e., $\mathrm{card}(\mathrm{PLift}\,\alpha) = \mathrm{card}(\alpha)$.

ENat.card_image_of_injOn theorem

{α β : Type*} {f : α → β} {s : Set α} (h : Set.InjOn f s) : card (f '' s) = card s

Full source

theorem card_image_of_injOn {α β : Type*} {f : α → β} {s : Set α} (h : Set.InjOn f s) :
    card (f '' s) = card s :=
  card_congr (Equiv.Set.imageOfInjOn f s h).symm

Cardinality Preservation under Injective Image: $\mathrm{card}(f(s)) = \mathrm{card}(s)$ for $f$ injective on $s$

Informal description

For any types $\alpha$ and $\beta$, a function $f : \alpha \to \beta$, and a subset $s \subseteq \alpha$, if $f$ is injective on $s$, then the extended natural number cardinality of the image $f(s)$ equals the extended natural number cardinality of $s$, i.e., $\mathrm{card}(f(s)) = \mathrm{card}(s)$.

ENat.card_image_of_injective theorem

{α β : Type*} (f : α → β) (s : Set α) (h : Function.Injective f) : card (f '' s) = card s

Full source

theorem card_image_of_injective {α β : Type*} (f : α → β) (s : Set α)
    (h : Function.Injective f) : card (f '' s) = card s := card_image_of_injOn h.injOn

Cardinality Preservation under Injective Image: $\mathrm{card}(f(s)) = \mathrm{card}(s)$ for injective $f$

Informal description

For any types $\alpha$ and $\beta$, a function $f \colon \alpha \to \beta$, and a subset $s \subseteq \alpha$, if $f$ is injective, then the extended natural number cardinality of the image $f(s)$ equals the extended natural number cardinality of $s$, i.e., $\mathrm{card}(f(s)) = \mathrm{card}(s)$.

Cardinal.natCast_le_toENat_iff theorem

{n : ℕ} {c : Cardinal} : ↑n ≤ toENat c ↔ ↑n ≤ c

Full source

@[simp]
theorem _root_.Cardinal.natCast_le_toENat_iff {n : ℕ} {c : Cardinal} :
    ↑n ≤ toENat c ↔ ↑n ≤ c := by
  rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 (le_of_lt (nat_lt_aleph0 n))]

Natural Number vs. Cardinal Comparison via Extended Naturals: $n \leq \mathrm{toENat}(c) \leftrightarrow n \leq c$

Informal description

For any natural number $n$ and cardinal number $c$, the inequality $n \leq \mathrm{toENat}(c)$ holds if and only if $n \leq c$ as cardinal numbers.

Cardinal.toENat_le_natCast_iff theorem

{c : Cardinal} {n : ℕ} : toENat c ≤ n ↔ c ≤ n

Full source

theorem _root_.Cardinal.toENat_le_natCast_iff {c : Cardinal} {n : ℕ} :
    toENattoENat c ≤ n ↔ c ≤ n := by simp

Inequality between Cardinal's Extended Natural Projection and Natural Number Cast

Informal description

For any cardinal number $c$ and natural number $n$, the extended natural number obtained from $c$ via the `toENat` function is less than or equal to $n$ if and only if $c$ itself is less than or equal to $n$.

Cardinal.natCast_eq_toENat_iff theorem

{n : ℕ} {c : Cardinal} : ↑n = toENat c ↔ ↑n = c

Full source

@[simp]
theorem _root_.Cardinal.natCast_eq_toENat_iff {n : ℕ} {c : Cardinal} :
    ↑n = toENat c ↔ ↑n = c := by
  rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toENat_le_natCast_iff,
    Cardinal.natCast_le_toENat_iff]

Equality between Natural Number Cast and Cardinal Projection in Extended Naturals

Informal description

For any natural number $n$ and cardinal number $c$, the extended natural number obtained from casting $n$ equals the extended natural projection of $c$ if and only if the cardinal number obtained from casting $n$ equals $c$. In symbols: $$n = \mathrm{toENat}(c) \leftrightarrow n = c$$

Cardinal.toENat_eq_natCast_iff theorem

{c : Cardinal} {n : ℕ} : Cardinal.toENat c = n ↔ c = n

Full source

theorem _root_.Cardinal.toENat_eq_natCast_iff {c : Cardinal} {n : ℕ} :
    Cardinal.toENatCardinal.toENat c = n ↔ c = n := by simp

Equivalence of Cardinal Projection and Natural Number Cast

Informal description

For any cardinal number $c$ and natural number $n$, the extended natural number projection of $c$ equals $n$ if and only if $c$ equals $n$. In other words, $\mathrm{toENat}(c) = n \leftrightarrow c = n$.

Cardinal.natCast_lt_toENat_iff theorem

{n : ℕ} {c : Cardinal} : ↑n < toENat c ↔ ↑n < c

Full source

@[simp]
theorem _root_.Cardinal.natCast_lt_toENat_iff {n : ℕ} {c : Cardinal} :
    ↑n < toENat c ↔ ↑n < c := by
  simp only [← not_le, Cardinal.toENat_le_natCast_iff]

Natural Number Cast vs Cardinal Projection Inequality in Extended Naturals

Informal description

For any natural number $n$ and cardinal number $c$, the extended natural number corresponding to $n$ is less than the extended natural number projection of $c$ if and only if the cardinal number corresponding to $n$ is less than $c$ in the cardinal order. In symbols: $$\uparrow n < \mathrm{toENat}(c) \leftrightarrow \uparrow n < c$$

Cardinal.toENat_lt_natCast_iff theorem

{n : ℕ} {c : Cardinal} : toENat c < ↑n ↔ c < ↑n

Full source

@[simp]
theorem _root_.Cardinal.toENat_lt_natCast_iff {n : ℕ} {c : Cardinal} :
    toENattoENat c < ↑n ↔ c < ↑n := by
  simp only [← not_le, Cardinal.natCast_le_toENat_iff]

Projection to Extended Natural Numbers Preserves Order with Natural Numbers

Informal description

For any natural number $n$ and cardinal number $c$, the extended natural number obtained from $c$ via the projection $\mathrm{toENat}$ is less than $n$ if and only if $c$ is less than $n$ as a cardinal number.

ENat.card_eq_zero_iff_empty theorem

(α : Type*) : card α = 0 ↔ IsEmpty α

Full source

theorem card_eq_zero_iff_empty (α : Type*) : cardcard α = 0 ↔ IsEmpty α := by
  rw [← Cardinal.mk_eq_zero_iff]
  simp [card]

Characterization of Zero Cardinality in Extended Naturals: $\mathrm{card}(\alpha) = 0 \leftrightarrow \text{IsEmpty}\,\alpha$

Informal description

For any type $\alpha$, the extended natural number cardinality of $\alpha$ is equal to $0$ if and only if $\alpha$ is an empty type (i.e., $\alpha$ has no elements). In symbols: $$\mathrm{card}(\alpha) = 0 \leftrightarrow \text{IsEmpty}\,\alpha$$

ENat.card_le_one_iff_subsingleton theorem

(α : Type*) : card α ≤ 1 ↔ Subsingleton α

Full source

theorem card_le_one_iff_subsingleton (α : Type*) : cardcard α ≤ 1 ↔ Subsingleton α := by
  rw [← le_one_iff_subsingleton]
  simp [card]

Subsingleton Criterion via Extended Cardinality: $\text{card}(\alpha) \leq 1 \leftrightarrow \text{Subsingleton}(\alpha)$

Informal description

For any type $\alpha$, the cardinality of $\alpha$ as an extended natural number is less than or equal to $1$ if and only if $\alpha$ is a subsingleton (i.e., any two elements of $\alpha$ are equal).

ENat.one_lt_card_iff_nontrivial theorem

(α : Type*) : 1 < card α ↔ Nontrivial α

Full source

theorem one_lt_card_iff_nontrivial (α : Type*) : 1 < card α ↔ Nontrivial α := by
  rw [← Cardinal.one_lt_iff_nontrivial]
  conv_rhs => rw [← Nat.cast_one]
  rw [← natCast_lt_toENat_iff]
  simp only [ENat.card, Nat.cast_one]

Extended Cardinality Greater Than One iff Nontrivial Type

Informal description

For any type $\alpha$, the extended natural number 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). In symbols: $$1 < \mathrm{card}(\alpha) \leftrightarrow \text{Nontrivial }\alpha$$

ENat.card_prod theorem

(α β : Type*) : ENat.card (α × β) = .card α * .card β

Full source

@[simp]
theorem card_prod (α β : Type*) : ENat.card (α × β) = .card α * .card β := by
  simp [ENat.card]

Product Cardinality Formula for Extended Natural Numbers: $\mathrm{card}(\alpha \times \beta) = \mathrm{card}(\alpha) \cdot \mathrm{card}(\beta)$

Informal description

For any types $\alpha$ and $\beta$, the extended natural number cardinality of their product $\alpha \times \beta$ is equal to the product of their individual cardinalities, i.e., $$\mathrm{card}(\alpha \times \beta) = \mathrm{card}(\alpha) \cdot \mathrm{card}(\beta).$$ Here, $\mathrm{card}(\cdot)$ denotes the extended natural number cardinality, which is finite for finite types and $\infty$ for infinite types.

Main Definitions