Mathlib.SetTheory.Cardinal.Defs

Cardinal.isEquivalent instance

: Setoid (Type u)

Full source

/-- The equivalence relation on types given by equivalence (bijective correspondence) of types.
  Quotienting by this equivalence relation gives the cardinal numbers.
-/
instance Cardinal.isEquivalent : Setoid (Type u) where
  r α β := Nonempty (α ≃ β)
  iseqv := ⟨
    fun α => ⟨Equiv.refl α⟩,
    fun ⟨e⟩ => ⟨e.symm⟩,
    fun ⟨e₁⟩ ⟨e₂⟩ => ⟨e₁.trans e₂⟩⟩

Equinumerity as an Equivalence Relation on Types

Informal description

The relation of equinumerity (bijective correspondence) between types forms an equivalence relation on the universe of types. This equivalence relation is used to define cardinal numbers as the quotient of types under this relation.

Cardinal definition

: Type (u + 1)

Full source

/-- `Cardinal.{u}` is the type of cardinal numbers in `Type u`,
  defined as the quotient of `Type u` by existence of an equivalence
  (a bijection with explicit inverse). -/
@[pp_with_univ]
def Cardinal : Type (u + 1) :=
  Quotient Cardinal.isEquivalent

Cardinal Numbers

Informal description

The type `Cardinal.{u}` represents cardinal numbers in the universe `Type u`, defined as the quotient of types in `Type u` by the equivalence relation of equinumerity (existence of a bijection between types).

Cardinal.mk definition

: Type u → Cardinal

Full source

/-- The cardinal number of a type -/
def mk : Type u → Cardinal :=
  Quotient.mk'

Cardinality of a type

Informal description

The function maps a type $\alpha$ to its cardinality, denoted $\#\alpha$, which is the equivalence class of $\alpha$ under the relation of equinumerity (existence of a bijection between types).

Cardinal.term#_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped prefix:max "#" => Cardinal.mk

Cardinality notation `#α`

Informal description

The notation `#α` denotes the cardinality of a type `α`, which is the equivalence class of `α` under the relation of equinumerity (bijective correspondence). This notation is defined as a prefix operator that applies the function `Cardinal.mk` to a type.

Cardinal.canLiftCardinalType instance

: CanLift Cardinal.{u} (Type u) mk fun _ => True

Full source

instance canLiftCardinalType : CanLift CardinalCardinal.{u} (Type u) mk fun _ => True :=
  ⟨fun c _ => Quot.inductionOn c fun α => ⟨α, rfl⟩⟩

Lifting Cardinal Numbers to Types

Informal description

For any universe level $u$, there exists a lifting condition from the type of cardinal numbers $\text{Cardinal.\{u\}}$ to the type $\text{Type u}$, where the lifting function is the cardinality function $\text{mk}$ (mapping a type to its cardinality) and the condition is always satisfied (i.e., any cardinal can be lifted from a type in $\text{Type u}$).

Cardinal.inductionOn theorem

{p : Cardinal → Prop} (c : Cardinal) (h : ∀ α, p #α) : p c

Full source

@[elab_as_elim]
theorem inductionOn {p : Cardinal → Prop} (c : Cardinal) (h : ∀ α, p #α) : p c :=
  Quotient.inductionOn c h

Induction Principle for Cardinal Numbers

Informal description

For any predicate $p$ on cardinal numbers and any cardinal number $c$, if $p(\#\alpha)$ holds for every type $\alpha$, then $p(c)$ holds. Here $\#\alpha$ denotes the cardinality of the type $\alpha$.

Cardinal.inductionOn₂ theorem

{p : Cardinal → Cardinal → Prop} (c₁ : Cardinal) (c₂ : Cardinal) (h : ∀ α β, p #α #β) : p c₁ c₂

Full source

@[elab_as_elim]
theorem inductionOn₂ {p : Cardinal → Cardinal → Prop} (c₁ : Cardinal) (c₂ : Cardinal)
    (h : ∀ α β, p #α #β) : p c₁ c₂ :=
  Quotient.inductionOn₂ c₁ c₂ h

Double Induction Principle for Cardinal Numbers

Informal description

For any predicate $p$ on pairs of cardinal numbers and any two cardinal numbers $c_1$ and $c_2$, if $p(\#\alpha, \#\beta)$ holds for all types $\alpha$ and $\beta$, then $p(c_1, c_2)$ holds. Here $\#\alpha$ denotes the cardinality of the type $\alpha$.

Cardinal.inductionOn₃ theorem

 {p : Cardinal → Cardinal → Cardinal → Prop} (c₁ : Cardinal) (c₂ : Cardinal) (c₃ : Cardinal) (h : ∀ α β γ, p #α #β #γ) :
  p c₁ c₂ c₃

Full source

@[elab_as_elim]
theorem inductionOn₃ {p : Cardinal → Cardinal → Cardinal → Prop} (c₁ : Cardinal) (c₂ : Cardinal)
    (c₃ : Cardinal) (h : ∀ α β γ, p #α #β #γ) : p c₁ c₂ c₃ :=
  Quotient.inductionOn₃ c₁ c₂ c₃ h

Triple Induction Principle for Cardinal Numbers

Informal description

For any predicate $p$ on three cardinal numbers and any cardinal numbers $c_1, c_2, c_3$, if $p(\#\alpha, \#\beta, \#\gamma)$ holds for all types $\alpha, \beta, \gamma$, then $p(c_1, c_2, c_3)$ holds. Here $\#\alpha$ denotes the cardinality of the type $\alpha$.

Cardinal.induction_on_pi theorem

 {ι : Type u} {p : (ι → Cardinal.{v}) → Prop} (f : ι → Cardinal.{v}) (h : ∀ f : ι → Type v, p fun i ↦ #(f i)) : p f

Full source

theorem induction_on_pi {ι : Type u} {p : (ι → CardinalCardinal.{v}) → Prop}
    (f : ι → CardinalCardinal.{v}) (h : ∀ f : ι → Type v, p fun i ↦ #(f i)) : p f :=
  Quotient.induction_on_pi f h

Induction Principle for Cardinal-Valued Functions

Informal description

Let $\iota$ be a type and $p$ be a predicate on functions from $\iota$ to cardinal numbers. For any function $f \colon \iota \to \text{Cardinal}$, if $p$ holds for all functions of the form $\lambda i, \#(g(i))$ where $g \colon \iota \to \text{Type}$, then $p$ holds for $f$.

Cardinal.eq theorem

: #α = #β ↔ Nonempty (α ≃ β)

Full source

protected theorem eq : #α#α = #β ↔ Nonempty (α ≃ β) :=
  Quotient.eq'

Cardinal Equality via Bijection

Informal description

For any 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 symbols: $$\#\alpha = \#\beta \leftrightarrow \text{Nonempty } (\alpha \simeq \beta)$$

Cardinal.mk_out theorem

(c : Cardinal) : #c.out = c

Full source

@[simp]
theorem mk_out (c : Cardinal) : #c.out = c :=
  Quotient.out_eq _

Cardinality of Quotient Representative Equals Original Cardinal

Informal description

For any cardinal number $c$, the cardinality of the representative type selected by the quotient operation (denoted $c.\mathrm{out}$) is equal to $c$ itself, i.e., $\#(c.\mathrm{out}) = c$.

Cardinal.outMkEquiv definition

{α : Type v} : (#α).out ≃ α

Full source

/-- The representative of the cardinal of a type is equivalent to the original type. -/
def outMkEquiv {α : Type v} : (#α).out ≃ α :=
  Nonempty.some <| Cardinal.eq.mp (by simp)

Bijection between cardinal representative and original type

Informal description

For any type $\alpha$, the representative type selected from the equivalence class of $\alpha$'s cardinality (denoted $(\#\alpha).\mathrm{out}$) is in bijective correspondence with $\alpha$ itself. In other words, there exists a bijection between the quotient representative of $\#\alpha$ and the original type $\alpha$.

Cardinal.mk_congr theorem

(e : α ≃ β) : #α = #β

Full source

theorem mk_congr (e : α ≃ β) : #α = #β :=
  Quot.sound ⟨e⟩

Equinumerous Types Have Equal Cardinality

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the cardinalities of $\alpha$ and $\beta$ are equal, i.e., $\#\alpha = \#\beta$.

Cardinal.map definition

(f : Type u → Type v) (hf : ∀ α β, α ≃ β → f α ≃ f β) : Cardinal.{u} → Cardinal.{v}

Full source

/-- Lift a function between `Type*`s to a function between `Cardinal`s. -/
def map (f : Type u → Type v) (hf : ∀ α β, α ≃ β → f α ≃ f β) : CardinalCardinal.{u} → CardinalCardinal.{v} :=
  Quotient.map f fun α β ⟨e⟩ => ⟨hf α β e⟩

Lifting type functions to cardinal numbers

Informal description

Given a function $f : \text{Type } u \to \text{Type } v$ that respects type equivalence (i.e., for any types $\alpha, \beta \in \text{Type } u$, if $\alpha \simeq \beta$ then $f(\alpha) \simeq f(\beta)$), the function $\text{Cardinal.map}$ lifts $f$ to a function between cardinal numbers $\text{Cardinal.{u}} \to \text{Cardinal.{v}}$. This is done by applying $f$ to representative types and preserving the equivalence relation of equinumerity.

Cardinal.map_mk theorem

(f : Type u → Type v) (hf : ∀ α β, α ≃ β → f α ≃ f β) (α : Type u) : map f hf #α = #(f α)

Full source

@[simp]
theorem map_mk (f : Type u → Type v) (hf : ∀ α β, α ≃ β → f α ≃ f β) (α : Type u) :
    map f hf #α = #(f α) :=
  rfl

Cardinality Preservation under Type Function Lifting: $\text{map } f \text{ hf } (\#\alpha) = \#(f \alpha)$

Informal description

Given a function $f : \text{Type } u \to \text{Type } v$ that respects type equivalence (i.e., for any types $\alpha, \beta \in \text{Type } u$, if $\alpha \simeq \beta$ then $f(\alpha) \simeq f(\beta)$), and a type $\alpha \in \text{Type } u$, the cardinality of the image of $\alpha$ under $f$ is equal to the image of the cardinality of $\alpha$ under the lifted function $\text{map } f \text{ hf}$. In other words, $\text{map } f \text{ hf } (\#\alpha) = \#(f \alpha)$.

Cardinal.map₂ definition

 (f : Type u → Type v → Type w) (hf : ∀ α β γ δ, α ≃ β → γ ≃ δ → f α γ ≃ f β δ) :
  Cardinal.{u} → Cardinal.{v} → Cardinal.{w}

Full source

/-- Lift a binary operation `Type* → Type* → Type*` to a binary operation on `Cardinal`s. -/
def map₂ (f : Type u → Type v → Type w) (hf : ∀ α β γ δ, α ≃ β → γ ≃ δ → f α γ ≃ f β δ) :
    CardinalCardinal.{u} → CardinalCardinal.{v} → CardinalCardinal.{w} :=
  Quotient.map₂ f fun α β ⟨e₁⟩ γ δ ⟨e₂⟩ => ⟨hf α β γ δ e₁ e₂⟩

Lifting binary operations to cardinal numbers

Informal description

Given a binary operation $f : \text{Type } u \to \text{Type } v \to \text{Type } w$ that respects type equivalence (i.e., for any types $\alpha, \beta \in \text{Type } u$ and $\gamma, \delta \in \text{Type } v$, if $\alpha \simeq \beta$ and $\gamma \simeq \delta$ then $f(\alpha, \gamma) \simeq f(\beta, \delta)$), the function $\text{Cardinal.map₂}$ lifts $f$ to a binary operation on cardinal numbers $\text{Cardinal.{u}} \to \text{Cardinal.{v}} \to \text{Cardinal.{w}}$. This is done by applying $f$ to representative types and preserving the equivalence relation of equinumerity.

Cardinal.lift definition

(c : Cardinal.{v}) : Cardinal.{max v u}

Full source

/-- The universe lift operation on cardinals. You can specify the universes explicitly with
  `lift.{u v} : Cardinal.{v} → Cardinal.{max v u}` -/
@[pp_with_univ]
def lift (c : CardinalCardinal.{v}) : CardinalCardinal.{max v u} :=
  map ULiftULift.{u, v} (fun _ _ e => Equiv.ulift.trans <| e.trans Equiv.ulift.symm) c

Universe lift operation on cardinals

Informal description

The function `Cardinal.lift` maps a cardinal number $ c $ in universe `Type v` to a cardinal number in the universe `Type (max v u)`, by lifting the underlying type of $ c $ using the `ULift` construction. Specifically, if $ c $ is the cardinality of a type $ \alpha $, then `lift c` is the cardinality of `ULift.{u, v} α`.

Cardinal.mk_uLift theorem

(α) : #(ULift.{v, u} α) = lift.{v} #α

Full source

@[simp]
theorem mk_uLift (α) : #(ULift.{v, u} α) = lift.{v} #α :=
  rfl

Cardinality of Lifted Type Equals Lifted Cardinality

Informal description

For any type $\alpha$ in universe `Type u`, the cardinality of the lifted type $\text{ULift.{v, u}} \alpha$ is equal to the lift of the cardinality of $\alpha$ to universe `Type (max u v)`, i.e., $\#(\text{ULift.{v, u}} \alpha) = \text{lift.{v}} (\#\alpha)$.

Cardinal.lift_umax theorem

: lift.{max u v, u} = lift.{v, u}

Full source

/-- `lift.{max u v, u}` equals `lift.{v, u}`.

Unfortunately, the simp lemma doesn't work. -/
theorem lift_umax : liftlift.{max u v, u} = liftlift.{v, u} :=
  funext fun a => inductionOn a fun _ => (Equiv.ulift.trans Equiv.ulift.symm).cardinal_eq

Equality of Maximal and Simple Universe Lifts for Cardinals

Informal description

For any universe levels $u$ and $v$, the cardinal lift operation $\text{lift}_{\max(u,v), u}$ is equal to $\text{lift}_{v, u}$.

Cardinal.lift_id' theorem

(a : Cardinal.{max u v}) : lift.{u} a = a

Full source

/-- A cardinal lifted to a lower or equal universe equals itself.

Unfortunately, the simp lemma doesn't work. -/
theorem lift_id' (a : CardinalCardinal.{max u v}) : lift.{u} a = a :=
  inductionOn a fun _ => mk_congr Equiv.ulift

Lift Identity for Cardinals in Higher Universes

Informal description

For any cardinal number $a$ in the universe $\text{Type}(\max(u, v))$, lifting $a$ to the same or a higher universe level $u$ results in $a$ itself, i.e., $\text{lift}_u(a) = a$.

Cardinal.lift_id theorem

(a : Cardinal) : lift.{u, u} a = a

Full source

/-- A cardinal lifted to the same universe equals itself. -/
@[simp]
theorem lift_id (a : Cardinal) : lift.{u, u} a = a :=
  lift_id'.{u, u} a

Identity Law for Cardinal Lifting in the Same Universe

Informal description

For any cardinal number $a$ in a universe level $u$, lifting $a$ to the same universe level $u$ results in $a$ itself, i.e., $\text{lift}_u(a) = a$.

Cardinal.lift_uzero theorem

(a : Cardinal.{u}) : lift.{0} a = a

Full source

/-- A cardinal lifted to the zero universe equals itself. -/
@[simp]
theorem lift_uzero (a : CardinalCardinal.{u}) : lift.{0} a = a :=
  lift_id'.{0, u} a

Lift to Zero Universe Preserves Cardinality

Informal description

For any cardinal number $a$ in universe level $u$, lifting $a$ to the zero universe level preserves its value, i.e., $\text{lift}_0(a) = a$.

Cardinal.lift_lift theorem

(a : Cardinal.{u_1}) : lift.{w} (lift.{v} a) = lift.{max v w} a

Full source

@[simp]
theorem lift_lift.{u_1} (a : CardinalCardinal.{u_1}) : lift.{w} (lift.{v} a) = lift.{max v w} a :=
  inductionOn a fun _ => (Equiv.ulift.trans <| Equiv.ulift.trans Equiv.ulift.symm).cardinal_eq

Lift Composition Identity for Cardinal Numbers: $\text{lift}_w \circ \text{lift}_v = \text{lift}_{\max(v,w)}$

Informal description

For any cardinal number $a$ in universe level $u_1$, lifting $a$ to universe level $v$ and then to level $w$ is equivalent to lifting $a$ directly to the maximum of $v$ and $w$. That is, $\text{lift}_w(\text{lift}_v(a)) = \text{lift}_{\max(v,w)}(a)$.

Cardinal.out_lift_equiv theorem

(a : Cardinal.{u}) : Nonempty ((lift.{v} a).out ≃ a.out)

Full source

theorem out_lift_equiv (a : CardinalCardinal.{u}) : Nonempty ((lift.{v} a).out ≃ a.out) := by
  rw [← mk_out a, ← mk_uLift, mk_out]
  exact ⟨outMkEquiv.trans Equiv.ulift⟩

Bijection between representatives of a cardinal and its lift

Informal description

For any cardinal number $a$ in universe level $u$, there exists a bijection between the representative type of the lifted cardinal $\text{lift}_{v}(a)$ (in universe level $\max(u,v)$) and the representative type of $a$ itself. In other words, the underlying types of $a$ and its lift are equinumerous.

Cardinal.lift_mk_eq theorem

{α : Type u} {β : Type v} : lift.{max v w} #α = lift.{max u w} #β ↔ Nonempty (α ≃ β)

Full source

theorem lift_mk_eq {α : Type u} {β : Type v} :
    liftlift.{max v w} #α = lift.{max u w} #β ↔ Nonempty (α ≃ β) :=
  Quotient.eq'.trans
    ⟨fun ⟨f⟩ => ⟨Equiv.ulift.symm.trans <| f.trans Equiv.ulift⟩, fun ⟨f⟩ =>
      ⟨Equiv.ulift.trans <| f.trans Equiv.ulift.symm⟩⟩

Equality of Lifted Cardinalities is Equivalent to Type Equivalence

Informal description

For any types $\alpha$ in universe $u$ and $\beta$ in universe $v$, the equality of the lifted cardinalities $\#\alpha$ and $\#\beta$ (lifted to universe $\max(u,v,w)$) is equivalent to the existence of a bijection between $\alpha$ and $\beta$. In symbols: $$\text{lift}_{\max(v,w)} \#\alpha = \text{lift}_{\max(u,w)} \#\beta \leftrightarrow \text{Nonempty} (\alpha \simeq \beta)$$

Cardinal.lift_mk_eq' theorem

{α : Type u} {β : Type v} : lift.{v} #α = lift.{u} #β ↔ Nonempty (α ≃ β)

Full source

/-- A variant of `Cardinal.lift_mk_eq` with specialized universes.
Because Lean often can not realize it should use this specialization itself,
we provide this statement separately so you don't have to solve the specialization problem either.
-/
theorem lift_mk_eq' {α : Type u} {β : Type v} : liftlift.{v} #α = lift.{u} #β ↔ Nonempty (α ≃ β) :=
  lift_mk_eq.{u, v, 0}

Equality of Lifted Cardinalities is Equivalent to Type Equivalence (Universe-Specialized Version)

Informal description

For any types $\alpha$ in universe $u$ and $\beta$ in universe $v$, the equality of the lifted cardinalities $\text{lift}_v \#\alpha = \text{lift}_u \#\beta$ holds if and only if there exists a bijection between $\alpha$ and $\beta$. Here $\text{lift}_v \#\alpha$ denotes the cardinality of $\alpha$ lifted to universe $v$, and similarly for $\text{lift}_u \#\beta$.

Cardinal.mk_congr_lift theorem

{α : Type u} {β : Type v} (e : α ≃ β) : lift.{v} #α = lift.{u} #β

Full source

theorem mk_congr_lift {α : Type u} {β : Type v} (e : α ≃ β) : lift.{v} #α = lift.{u} #β :=
  lift_mk_eq'.2 ⟨e⟩

Equality of Lifted Cardinalities under Type Equivalence

Informal description

For any types $\alpha$ in universe $u$ and $\beta$ in universe $v$, if there exists a bijection $e : \alpha \simeq \beta$, then the lifted cardinalities satisfy $\text{lift}_v \#\alpha = \text{lift}_u \#\beta$. Here $\text{lift}_v \#\alpha$ denotes the cardinality of $\alpha$ lifted to universe $v$, and similarly for $\text{lift}_u \#\beta$.

Cardinal.instZero instance

: Zero Cardinal.{u}

Full source

instance : Zero CardinalCardinal.{u} :=
  -- `PEmpty` might be more canonical, but this is convenient for defeq with natCast
  ⟨lift #(Fin 0)⟩

Zero Cardinal as the Cardinality of the Empty Type

Informal description

The type of cardinal numbers $\text{Cardinal}$ has a zero element, which is the cardinality of the empty type.

Cardinal.instInhabited instance

: Inhabited Cardinal.{u}

Full source

instance : Inhabited CardinalCardinal.{u} :=
  ⟨0⟩

Inhabited Type of Cardinal Numbers

Informal description

The type of cardinal numbers $\text{Cardinal}$ is inhabited.

Cardinal.mk_eq_zero theorem

(α : Type u) [IsEmpty α] : #α = 0

Full source

@[simp]
theorem mk_eq_zero (α : Type u) [IsEmpty α] : #α = 0 :=
  (Equiv.equivOfIsEmpty α (ULift (Fin 0))).cardinal_eq

Cardinality of Empty Type is Zero

Informal description

For any type $\alpha$ in universe $u$, if $\alpha$ is empty, then its cardinality $\#\alpha$ is equal to $0$.

Cardinal.lift_zero theorem

: lift 0 = 0

Full source

@[simp]
theorem lift_zero : lift 0 = 0 := mk_eq_zero _

Lift of Zero Cardinal is Zero

Informal description

The lift operation applied to the zero cardinal (the cardinality of the empty type) yields zero in any higher universe, i.e., $\text{lift}\,0 = 0$.

Cardinal.mk_eq_zero_iff theorem

{α : Type u} : #α = 0 ↔ IsEmpty α

Full source

theorem mk_eq_zero_iff {α : Type u} : #α#α = 0 ↔ IsEmpty α :=
  ⟨fun e =>
    let ⟨h⟩ := Quotient.exact e
    h.isEmpty,
    @mk_eq_zero α⟩

Characterization of Zero Cardinality: $\#\alpha = 0 \leftrightarrow \text{IsEmpty}\,\alpha$

Informal description

For any type $\alpha$ in universe $u$, the cardinality $\#\alpha$ is equal to $0$ if and only if $\alpha$ is an empty type (i.e., $\alpha$ has no elements).

Cardinal.mk_ne_zero_iff theorem

{α : Type u} : #α ≠ 0 ↔ Nonempty α

Full source

theorem mk_ne_zero_iff {α : Type u} : #α#α ≠ 0#α ≠ 0 ↔ Nonempty α :=
  (not_iff_not.2 mk_eq_zero_iff).trans not_isEmpty_iff

Nonzero Cardinality Characterizes Nonempty Types

Informal description

For any type $\alpha$ in universe $u$, the cardinality $\#\alpha$ is nonzero if and only if $\alpha$ is nonempty, i.e., $\#\alpha \neq 0 \leftrightarrow \text{Nonempty}\,\alpha$.

Cardinal.mk_ne_zero theorem

(α : Type u) [Nonempty α] : #α ≠ 0

Full source

@[simp]
theorem mk_ne_zero (α : Type u) [Nonempty α] : #α#α ≠ 0 :=
  mk_ne_zero_iff.2 ‹_›

Nonempty Types Have Nonzero Cardinality

Informal description

For any nonempty type $\alpha$ in universe $u$, the cardinality $\#\alpha$ is nonzero.

Cardinal.instOne instance

: One Cardinal.{u}

Full source

instance : One CardinalCardinal.{u} :=
  -- `PUnit` might be more canonical, but this is convenient for defeq with natCast
  ⟨lift #(Fin 1)⟩

The One Element in Cardinal Numbers

Informal description

The type of cardinal numbers $\text{Cardinal}$ has a distinguished element $1$ representing the cardinality of any singleton type.

Cardinal.instNontrivial instance

: Nontrivial Cardinal.{u}

Full source

instance : Nontrivial CardinalCardinal.{u} :=
  ⟨⟨1, 0, mk_ne_zero _⟩⟩

Nontriviality of Cardinal Numbers

Informal description

The type of cardinal numbers $\text{Cardinal}$ is nontrivial, meaning it contains at least two distinct elements.

Cardinal.mk_eq_one theorem

(α : Type u) [Subsingleton α] [Nonempty α] : #α = 1

Full source

theorem mk_eq_one (α : Type u) [Subsingleton α] [Nonempty α] : #α = 1 :=
  let ⟨_⟩ := nonempty_unique α; (Equiv.ofUnique α (ULift (Fin 1))).cardinal_eq

Cardinality of Nonempty Subsingleton Types is One

Informal description

For any type $\alpha$ that is a subsingleton (has at most one element) and is nonempty (has at least one element), the cardinality of $\alpha$ is equal to $1$, i.e., $\#\alpha = 1$.

Cardinal.instAdd instance

: Add Cardinal.{u}

Full source

instance : Add CardinalCardinal.{u} :=
  ⟨map₂ Sum fun _ _ _ _ => Equiv.sumCongr⟩

Addition Operation on Cardinal Numbers

Informal description

The type of cardinal numbers $\text{Cardinal}$ is equipped with a canonical addition operation, where the sum of two cardinals $\#\alpha$ and $\#\beta$ is defined as the cardinality of the sum type $\alpha \oplus \beta$.

Cardinal.add_def theorem

(α β : Type u) : #α + #β = #(α ⊕ β)

Full source

theorem add_def (α β : Type u) : #α + #β = #(α ⊕ β) :=
  rfl

Cardinal Addition as Coproduct Cardinality

Informal description

For any two types $\alpha$ and $\beta$ in the same universe, the sum of their cardinalities $\#\alpha + \#\beta$ is equal to the cardinality of their coproduct (sum type) $\alpha \oplus \beta$. That is, $\#\alpha + \#\beta = \#(\alpha \oplus \beta)$.

Cardinal.instNatCast instance

: NatCast Cardinal.{u}

Full source

instance : NatCast CardinalCardinal.{u} :=
  ⟨fun n => lift #(Fin n)⟩

Natural Numbers as Cardinal Numbers

Informal description

The type of cardinal numbers $\text{Cardinal}$ is equipped with a canonical embedding of the natural numbers, where each natural number $n$ is mapped to the cardinality of a type with $n$ elements.

Cardinal.mk_sum theorem

(α : Type u) (β : Type v) : #(α ⊕ β) = lift.{v, u} #α + lift.{u, v} #β

Full source

@[simp]
theorem mk_sum (α : Type u) (β : Type v) : #(α ⊕ β) = lift.{v, u} #α + lift.{u, v} #β :=
  mk_congr (Equiv.ulift.symm.sumCongr Equiv.ulift.symm)

Cardinality of Sum Type Equals Sum of Lifted Cardinalities

Informal description

For any types $\alpha$ in universe $u$ and $\beta$ in universe $v$, the cardinality of the sum type $\alpha \oplus \beta$ is equal to the sum of the lifted cardinalities of $\alpha$ and $\beta$, where $\#\alpha$ is lifted to universe $\max(u,v)$ and $\#\beta$ is lifted to universe $\max(u,v)$. That is, $$\#(\alpha \oplus \beta) = \text{lift}_{v,u}(\#\alpha) + \text{lift}_{u,v}(\#\beta).$$

Cardinal.mk_option theorem

{α : Type u} : #(Option α) = #α + 1

Full source

@[simp]
theorem mk_option {α : Type u} : #(Option α) = #α + 1 := by
  rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]

Cardinality of Option Type: $\#(\text{Option }\alpha) = \#\alpha + 1$

Informal description

For any type $\alpha$ in universe $u$, the cardinality of the option type $\text{Option }\alpha$ is equal to the cardinality of $\alpha$ plus one, i.e., $\#(\text{Option }\alpha) = \#\alpha + 1$.

Cardinal.mk_psum theorem

(α : Type u) (β : Type v) : #(α ⊕' β) = lift.{v} #α + lift.{u} #β

Full source

@[simp]
theorem mk_psum (α : Type u) (β : Type v) : #(α ⊕' β) = lift.{v} #α + lift.{u} #β :=
  (mk_congr (Equiv.psumEquivSum α β)).trans (mk_sum α β)

Cardinality of Parallel Sum Type Equals Sum of Lifted Cardinalities

Informal description

For any types $\alpha$ in universe $u$ and $\beta$ in universe $v$, the cardinality of the parallel sum type $\alpha \oplus' \beta$ is equal to the sum of the lifted cardinalities of $\alpha$ and $\beta$, where $\#\alpha$ is lifted to universe $\max(u,v)$ and $\#\beta$ is lifted to universe $\max(u,v)$. That is, $$\#(\alpha \oplus' \beta) = \text{lift}_{v}(\#\alpha) + \text{lift}_{u}(\#\beta).$$

Cardinal.instMul instance

: Mul Cardinal.{u}

Full source

instance : Mul CardinalCardinal.{u} :=
  ⟨map₂ Prod fun _ _ _ _ => Equiv.prodCongr⟩

Multiplication Operation on Cardinal Numbers

Informal description

The type of cardinal numbers `Cardinal.{u}` is equipped with a multiplication operation, where the product of two cardinals `#α` and `#β` is defined as the cardinality of the product type `α × β`.

Cardinal.mul_def theorem

(α β : Type u) : #α * #β = #(α × β)

Full source

theorem mul_def (α β : Type u) : #α * #β = #(α × β) :=
  rfl

Cardinal Multiplication as Product Type Cardinality

Informal description

For any two types $\alpha$ and $\beta$ in the same universe, the product of their cardinalities $\#\alpha \cdot \#\beta$ equals the cardinality of their product type $\alpha \times \beta$, i.e., $\#(\alpha \times \beta)$.

Cardinal.mk_prod theorem

(α : Type u) (β : Type v) : #(α × β) = lift.{v, u} #α * lift.{u, v} #β

Full source

@[simp]
theorem mk_prod (α : Type u) (β : Type v) : #(α × β) = lift.{v, u} #α * lift.{u, v} #β :=
  mk_congr (Equiv.ulift.symm.prodCongr Equiv.ulift.symm)

Cardinality of Product Type via Lifted Cardinal Multiplication

Informal description

For any types $\alpha$ in universe $u$ and $\beta$ in universe $v$, the cardinality of their product type $\alpha \times \beta$ equals the product of the lifted cardinalities: $\#(\alpha \times \beta) = \text{lift}_{v,u}(\#\alpha) \cdot \text{lift}_{u,v}(\#\beta)$, where $\text{lift}_{v,u}$ and $\text{lift}_{u,v}$ are the universe lifting operations for cardinals.

Cardinal.instPowCardinal instance

: Pow Cardinal.{u} Cardinal.{u}

Full source

/-- The cardinal exponential. `#α ^ #β` is the cardinal of `β → α`. -/
instance instPowCardinal : Pow CardinalCardinal.{u} CardinalCardinal.{u} :=
  ⟨map₂ (fun α β => β → α) fun _ _ _ _ e₁ e₂ => e₂.arrowCongr e₁⟩

Cardinal Exponentiation as Function Space Cardinality

Informal description

For any two cardinal numbers $\kappa$ and $\lambda$ in the same universe, the exponentiation $\kappa^\lambda$ is defined as the cardinality of the function space $\lambda \to \kappa$.

Cardinal.power_def theorem

(α β : Type u) : #α ^ #β = #(β → α)

Full source

theorem power_def (α β : Type u) : #α ^ #β = #(β → α) :=
  rfl

Cardinal Exponentiation as Function Space Cardinality: $\#\alpha^{\#\beta} = \#(\beta \to \alpha)$

Informal description

For any types $\alpha$ and $\beta$ in the same universe, the cardinal exponentiation $\#\alpha^{\#\beta}$ is equal to the cardinality of the function space $\beta \to \alpha$, i.e., $\#(\beta \to \alpha)$.

Cardinal.mk_arrow theorem

(α : Type u) (β : Type v) : #(α → β) = (lift.{u} #β ^ lift.{v} #α)

Full source

theorem mk_arrow (α : Type u) (β : Type v) : #(α → β) = (lift.{u} #β^lift.{v} #α) :=
  mk_congr (Equiv.ulift.symm.arrowCongr Equiv.ulift.symm)

Cardinality of Function Space as Lifted Exponentiation

Informal description

For any types $\alpha$ (in universe $u$) and $\beta$ (in universe $v$), the cardinality of the function space $\alpha \to \beta$ is equal to the cardinality of $\beta$ lifted to universe $\max(u,v)$ raised to the power of the cardinality of $\alpha$ lifted to universe $\max(u,v)$. In symbols: $$\#(\alpha \to \beta) = (\text{lift}_{u}(\#\beta))^{\text{lift}_{v}(\#\alpha)}$$

Cardinal.lift_power theorem

(a b : Cardinal.{u}) : lift.{v} (a ^ b) = lift.{v} a ^ lift.{v} b

Full source

@[simp]
theorem lift_power (a b : CardinalCardinal.{u}) : lift.{v} (a ^ b) = lift.{v} a ^ lift.{v} b :=
  inductionOn₂ a b fun _ _ =>
    mk_congr <| Equiv.ulift.trans (Equiv.ulift.arrowCongr Equiv.ulift).symm

Lift of Cardinal Exponentiation Equals Exponentiation of Lifts

Informal description

For any two cardinal numbers $a$ and $b$ in the same universe, the lift of the exponentiation $a^b$ to a higher universe equals the exponentiation of the lifts of $a$ and $b$ in that higher universe. That is, $\text{lift}(a^b) = \text{lift}(a)^{\text{lift}(b)}$.

Cardinal.power_zero theorem

(a : Cardinal) : a ^ (0 : Cardinal) = 1

Full source

@[simp]
theorem power_zero (a : Cardinal) : a ^ (0 : Cardinal) = 1 :=
  inductionOn a fun _ => mk_eq_one _

Exponentiation Identity: $a^0 = 1$

Informal description

For any cardinal number $a$, the exponentiation $a^0$ equals $1$.

Cardinal.power_one theorem

(a : Cardinal.{u}) : a ^ (1 : Cardinal) = a

Full source

@[simp]
theorem power_one (a : CardinalCardinal.{u}) : a ^ (1 : Cardinal) = a :=
  inductionOn a fun α => mk_congr (Equiv.funUnique (ULift.{u} (Fin 1)) α)

Exponentiation Identity: $a^1 = a$

Informal description

For any cardinal number $a$, the exponentiation $a^1$ is equal to $a$.

Cardinal.power_add theorem

(a b c : Cardinal) : a ^ (b + c) = a ^ b * a ^ c

Full source

theorem power_add (a b c : Cardinal) : a ^ (b + c) = a ^ b * a ^ c :=
  inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumArrowEquivProdArrow β γ α

Exponentiation Law for Cardinal Addition: $a^{b + c} = a^b \cdot a^c$

Informal description

For any cardinal numbers $a$, $b$, and $c$, the exponentiation $a^{b + c}$ is equal to the product $a^b \cdot a^c$.

Cardinal.one_power theorem

{a : Cardinal} : (1 : Cardinal) ^ a = 1

Full source

@[simp]
theorem one_power {a : Cardinal} : (1 : Cardinal) ^ a = 1 :=
  inductionOn a fun _ => mk_eq_one _

Exponentiation Identity: $1^a = 1$ for any cardinal $a$

Informal description

For any cardinal number $a$, the exponentiation of $1$ raised to the power of $a$ is equal to $1$, i.e., $1^a = 1$.

Cardinal.zero_power theorem

{a : Cardinal} : a ≠ 0 → (0 : Cardinal) ^ a = 0

Full source

@[simp]
theorem zero_power {a : Cardinal} : a ≠ 0 → (0 : Cardinal) ^ a = 0 :=
  inductionOn a fun _ heq =>
    mk_eq_zero_iff.2 <|
      isEmpty_pi.2 <|
        let ⟨a⟩ := mk_ne_zero_iff.1 heq
        ⟨a, inferInstance⟩

Zero to a Nonzero Power is Zero: $0^a = 0$ for $a \neq 0$

Informal description

For any nonzero cardinal number $a$, the zero cardinal raised to the power of $a$ is equal to the zero cardinal, i.e., $0^a = 0$.

Cardinal.power_ne_zero theorem

{a : Cardinal} (b : Cardinal) : a ≠ 0 → a ^ b ≠ 0

Full source

theorem power_ne_zero {a : Cardinal} (b : Cardinal) : a ≠ 0 → a ^ b ≠ 0 :=
  inductionOn₂ a b fun _ _ h =>
    let ⟨a⟩ := mk_ne_zero_iff.1 h
    mk_ne_zero_iff.2 ⟨fun _ => a⟩

Nonzero Cardinal Exponentiation: $a \neq 0 \Rightarrow a^b \neq 0$

Informal description

For any cardinal numbers $a$ and $b$, if $a$ is nonzero, then the exponentiation $a^b$ is also nonzero.

Cardinal.mul_power theorem

{a b c : Cardinal} : (a * b) ^ c = a ^ c * b ^ c

Full source

theorem mul_power {a b c : Cardinal} : (a * b) ^ c = a ^ c * b ^ c :=
  inductionOn₃ a b c fun _ _ γ => mk_congr <| Equiv.arrowProdEquivProdArrow γ _ _

Exponentiation of Product of Cardinals: $(a \cdot b)^c = a^c \cdot b^c$

Informal description

For any cardinal numbers $a$, $b$, and $c$, the exponentiation of their product satisfies $(a \cdot b)^c = a^c \cdot b^c$.

Cardinal.lift_one theorem

: lift 1 = 1

Full source

@[simp]
theorem lift_one : lift 1 = 1 := mk_eq_one _

Universe Lift Preserves the Cardinal One

Informal description

The lift of the cardinal number $1$ to any higher universe is equal to $1$, i.e., $\text{lift}(1) = 1$.

Cardinal.lift_add theorem

(a b : Cardinal.{u}) : lift.{v} (a + b) = lift.{v} a + lift.{v} b

Full source

@[simp]
theorem lift_add (a b : CardinalCardinal.{u}) : lift.{v} (a + b) = lift.{v} a + lift.{v} b :=
  inductionOn₂ a b fun _ _ =>
    mk_congr <| Equiv.ulift.trans (Equiv.sumCongr Equiv.ulift Equiv.ulift).symm

Lift Distributes Over Addition of Cardinals

Informal description

For any two cardinal numbers $a$ and $b$ in universe level $u$, the lift of their sum to universe level $\max(u,v)$ equals the sum of their lifts. That is, $\text{lift}(a + b) = \text{lift}(a) + \text{lift}(b)$.

Cardinal.sum definition

{ι} (f : ι → Cardinal) : Cardinal

Full source

/-- The indexed sum of cardinals is the cardinality of the
  indexed disjoint union, i.e. sigma type. -/
def sum {ι} (f : ι → Cardinal) : Cardinal :=
  mk (Σ i, (f i).out)

Indexed sum of cardinals

Informal description

The indexed sum of a family of cardinals $(κ_i)_{i \in ι}$ is the cardinality of the corresponding sigma type $\Sigma i, \alpha_i$, where each $\alpha_i$ is a representative of the cardinal $κ_i$.

Cardinal.mk_sigma theorem

{ι} (f : ι → Type*) : #(Σ i, f i) = sum fun i => #(f i)

Full source

@[simp]
theorem mk_sigma {ι} (f : ι → Type*) : #(Σ i, f i) = sum fun i => #(f i) :=
  mk_congr <| Equiv.sigmaCongrRight fun _ => outMkEquiv.symm

Cardinality of Dependent Sum Equals Sum of Cardinalities

Informal description

For any family of types $(f_i)_{i \in \iota}$ indexed by a type $\iota$, the cardinality of the dependent sum type $\Sigma i, f_i$ is equal to the sum of the cardinalities of the individual types $f_i$. That is, $\#(\Sigma i, f_i) = \sum_{i \in \iota} \#(f_i)$.

Cardinal.mk_sigma_congr_lift theorem

 {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι')
  (h : ∀ i, lift.{w'} #(f i) = lift.{w} #(g (e i))) : lift.{max v' w'} #(Σ i, f i) = lift.{max v w} #(Σ i, g i)

Full source

theorem mk_sigma_congr_lift {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'}
    (e : ι ≃ ι') (h : ∀ i, lift.{w'} #(f i) = lift.{w} #(g (e i))) :
    lift.{max v' w'} #(Σ i, f i) = lift.{max v w} #(Σ i, g i) :=
  Cardinal.lift_mk_eq'.2 ⟨.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.lift_mk_eq'.1 (h i)⟩

Equality of Lifted Cardinalities of Dependent Sums under Index Bijection and Fiberwise Equinumerity

Informal description

Let $\iota$ and $\iota'$ be types in universes $v$ and $v'$ respectively, and let $f : \iota \to \text{Type}_w$ and $g : \iota' \to \text{Type}_{w'}$ be families of types. Given a bijection $e : \iota \simeq \iota'$ such that for each $i \in \iota$, the lifted cardinality of $f(i)$ (to universe $w'$) equals the lifted cardinality of $g(e(i))$ (to universe $w$), then the lifted cardinality of the dependent sum $\Sigma_{i \in \iota} f(i)$ (to universe $\max v' w'$) equals the lifted cardinality of the dependent sum $\Sigma_{i \in \iota'} g(i)$ (to universe $\max v w$). In symbols: $$\left( \forall i, \text{lift}_{w'} \#(f(i)) = \text{lift}_w \#(g(e(i))) \right) \implies \text{lift}_{\max v' w'} \#\left( \Sigma_{i \in \iota} f(i) \right) = \text{lift}_{\max v w} \#\left( \Sigma_{i \in \iota'} g(i) \right)$$

Cardinal.mk_sigma_congr theorem

 {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι') (h : ∀ i, #(f i) = #(g (e i))) :
  #(Σ i, f i) = #(Σ i, g i)

Full source

theorem mk_sigma_congr {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι')
    (h : ∀ i, #(f i) = #(g (e i))) : #(Σ i, f i) = #(Σ i, g i) :=
  mk_congr <| Equiv.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

Equality of Dependent Sum Cardinalities under Index Bijection and Fiber-wise Equinumerosity

Informal description

Let $\iota$ and $\iota'$ be types in the same universe, and let $f : \iota \to \text{Type}_v$ and $g : \iota' \to \text{Type}_v$ be families of types. Given a bijection $e : \iota \simeq \iota'$ such that for each $i \in \iota$, the cardinality of $f(i)$ equals the cardinality of $g(e(i))$, then the cardinality of the dependent sum $\Sigma_{i \in \iota} f(i)$ equals the cardinality of the dependent sum $\Sigma_{i \in \iota'} g(i)$. In symbols: $$\#(\Sigma i, f i) = \#(\Sigma i, g i)$$

Cardinal.mk_sigma_congr' theorem

 {ι : Type u} {ι' : Type v} {f : ι → Type max w (max u v)} {g : ι' → Type max w (max u v)} (e : ι ≃ ι')
  (h : ∀ i, #(f i) = #(g (e i))) : #(Σ i, f i) = #(Σ i, g i)

Full source

/-- Similar to `mk_sigma_congr` with indexing types in different universes. This is not a strict
generalization. -/
theorem mk_sigma_congr' {ι : Type u} {ι' : Type v} {f : ι → Type max w (max u v)}
    {g : ι' → Type max w (max u v)} (e : ι ≃ ι')
    (h : ∀ i, #(f i) = #(g (e i))) : #(Σ i, f i) = #(Σ i, g i) :=
  mk_congr <| Equiv.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

Equality of Cardinalities of Dependent Sums under Index Bijection and Fiberwise Equinumerity

Informal description

Let $\iota$ and $\iota'$ be types in universes $u$ and $v$ respectively, and let $f : \iota \to \text{Type}_{\max w (\max u v)}$ and $g : \iota' \to \text{Type}_{\max w (\max u v)}$ be families of types. Given a bijection $e : \iota \simeq \iota'$ such that for every $i \in \iota$, the cardinality of $f(i)$ equals the cardinality of $g(e(i))$, then the cardinality of the dependent sum $\Sigma_{i \in \iota} f(i)$ equals the cardinality of the dependent sum $\Sigma_{i \in \iota'} g(i)$. In symbols: $$\left( \forall i, \#(f(i)) = \#(g(e(i))) \right) \implies \#\left( \Sigma_{i \in \iota} f(i) \right) = \#\left( \Sigma_{i \in \iota'} g(i) \right)$$

Cardinal.mk_sigma_congrRight theorem

{ι : Type u} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) : #(Σ i, f i) = #(Σ i, g i)

Full source

theorem mk_sigma_congrRight {ι : Type u} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) :
    #(Σ i, f i) = #(Σ i, g i) :=
  mk_sigma_congr (Equiv.refl ι) h

Equality of Dependent Sum Cardinalities under Fiberwise Equinumerity

Informal description

For any type $\iota$ and families of types $f, g : \iota \to \text{Type}_v$, if for every $i \in \iota$ the cardinality of $f(i)$ equals the cardinality of $g(i)$, then the cardinality of the dependent sum type $\Sigma_{i \in \iota} f(i)$ equals the cardinality of the dependent sum type $\Sigma_{i \in \iota} g(i)$. In symbols: $$(\forall i \in \iota, \#(f(i)) = \#(g(i))) \implies \#\left( \Sigma_{i \in \iota} f(i) \right) = \#\left( \Sigma_{i \in \iota} g(i) \right)$$

Cardinal.mk_psigma_congrRight theorem

{ι : Type u} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) : #(Σ' i, f i) = #(Σ' i, g i)

Full source

theorem mk_psigma_congrRight {ι : Type u} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) :
    #(Σ' i, f i) = #(Σ' i, g i) :=
  mk_congr <| .psigmaCongrRight fun i => Classical.choice <| Cardinal.eq.mp (h i)

Equality of Cardinalities of Dependent Sum Types under Componentwise Equinumerity

Informal description

For any type $\iota$ and families of types $f, g : \iota \to \text{Type}_v$, if for every $i \in \iota$ the cardinality of $f(i)$ equals the cardinality of $g(i)$, then the cardinality of the dependent sum type $\Sigma' i, f(i)$ equals the cardinality of the dependent sum type $\Sigma' i, g(i)$. In symbols: $$(\forall i, \#(f(i)) = \#(g(i))) \implies \#(\Sigma' i, f(i)) = \#(\Sigma' i, g(i))$$

Cardinal.mk_psigma_congrRight_prop theorem

{ι : Prop} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) : #(Σ' i, f i) = #(Σ' i, g i)

Full source

theorem mk_psigma_congrRight_prop {ι : Prop} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) :
    #(Σ' i, f i) = #(Σ' i, g i) :=
  mk_congr <| .psigmaCongrRight fun i => Classical.choice <| Cardinal.eq.mp (h i)

Equality of Cardinalities of Dependent Sum Types for Propositional Index

Informal description

Let $\iota$ be a proposition, and let $f, g : \iota \to \text{Type}_v$ be families of types indexed by $\iota$. If for every $i : \iota$, the cardinality of $f(i)$ equals the cardinality of $g(i)$, then the cardinality of the dependent sum type $\Sigma' i, f(i)$ equals the cardinality of the dependent sum type $\Sigma' i, g(i)$. In symbols: $$\forall i : \iota, \#(f(i)) = \#(g(i)) \implies \#(\Sigma' i, f(i)) = \#(\Sigma' i, g(i))$$

Cardinal.mk_sigma_arrow theorem

{ι} (α : Type*) (f : ι → Type*) : #(Sigma f → α) = #(Π i, f i → α)

Full source

theorem mk_sigma_arrow {ι} (α : Type*) (f : ι → Type*) :
    #(Sigma f → α) = #(Π i, f i → α) := mk_congr <| Equiv.piCurry fun _ _ ↦ α

Cardinality of Function Space from Sigma Type Equals Product of Function Spaces

Informal description

For any type $\alpha$ and any family of types $f : \iota \to \text{Type}^*$, the cardinality of the function space from the sigma type $\Sigma i, f i$ to $\alpha$ is equal to the cardinality of the product space $\prod_{i} (f i \to \alpha)$. In other words, $\#((\Sigma i, f i) \to \alpha) = \#(\prod_{i} (f i \to \alpha))$.

Cardinal.sum_const theorem

(ι : Type u) (a : Cardinal.{v}) : (sum fun _ : ι => a) = lift.{v} #ι * lift.{u} a

Full source

@[simp]
theorem sum_const (ι : Type u) (a : CardinalCardinal.{v}) :
    (sum fun _ : ι => a) = lift.{v} #ι * lift.{u} a :=
  inductionOn a fun α =>
    mk_congr <|
      calc
        (Σ _ : ι, Quotient.out #α) ≃ ι × Quotient.out #α := Equiv.sigmaEquivProd _ _
        _ ≃ ULift ι × ULift α := Equiv.ulift.symm.prodCongr (outMkEquiv.trans Equiv.ulift.symm)

Sum of Constant Cardinal Family Equals Product of Lifted Cardinals

Informal description

For any type $\iota$ in universe $u$ and any cardinal number $a$ in universe $v$, the sum of the constant family of cardinals $(\lambda \_, a)$ over $\iota$ is equal to the product of the lifted cardinality of $\iota$ (to universe $v$) and the lifted cardinal $a$ (to universe $u$). In symbols: $$\sum_{\_ : \iota} a = \text{lift}_{v}(\#\iota) \cdot \text{lift}_{u}(a)$$

Cardinal.sum_const' theorem

(ι : Type u) (a : Cardinal.{u}) : (sum fun _ : ι => a) = #ι * a

Full source

theorem sum_const' (ι : Type u) (a : CardinalCardinal.{u}) : (sum fun _ : ι => a) = #ι * a := by simp

Sum of Constant Cardinals in Same Universe Equals Product of Cardinalities

Informal description

For any type $\iota$ in universe $u$ and any cardinal number $a$ in the same universe, the sum of the constant family of cardinals $(\lambda \_, a)$ over $\iota$ is equal to the product of the cardinality of $\iota$ and $a$. In symbols: $$\sum_{\_ : \iota} a = \#\iota \cdot a$$

Cardinal.lift_sum theorem

 {ι : Type u} (f : ι → Cardinal.{v}) :
  Cardinal.lift.{w} (Cardinal.sum f) = Cardinal.sum fun i => Cardinal.lift.{w} (f i)

Full source

@[simp]
theorem lift_sum {ι : Type u} (f : ι → CardinalCardinal.{v}) :
    Cardinal.lift.{w} (Cardinal.sum f) = Cardinal.sum fun i => Cardinal.lift.{w} (f i) :=
  Equiv.cardinal_eq <|
    Equiv.ulift.trans <|
      Equiv.sigmaCongrRight fun a =>
    -- Porting note: Inserted universe hint .{_,_,v} below
        Nonempty.some <| by rw [← lift_mk_eq.{_,_,v}, mk_out, mk_out, lift_lift]

Lift Commutes with Sum of Cardinals: $\text{lift}_w(\sum_i f(i)) = \sum_i \text{lift}_w(f(i))$

Informal description

For any type $\iota$ in universe $u$ and any family of cardinals $f : \iota \to \text{Cardinal.\{v\}}$, lifting the sum of the family $f$ to universe $w$ is equal to the sum of the family where each cardinal $f(i)$ is lifted to universe $w$. In symbols: $$\text{lift}_w\left(\sum_{i \in \iota} f(i)\right) = \sum_{i \in \iota} \text{lift}_w(f(i))$$

Cardinal.sum_nat_eq_add_sum_succ theorem

(f : ℕ → Cardinal.{u}) : Cardinal.sum f = f 0 + Cardinal.sum fun i => f (i + 1)

Full source

theorem sum_nat_eq_add_sum_succ (f : ℕ → CardinalCardinal.{u}) :
    Cardinal.sum f = f 0 + Cardinal.sum fun i => f (i + 1) := by
  refine (Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans ?_
  simp only [mk_sum, mk_out, lift_id, mk_sigma]

Sum of Cardinal Sequence Equals First Term Plus Shifted Sum

Informal description

For any sequence of cardinal numbers $(f(n))_{n \in \mathbb{N}}$, the sum of the sequence equals the first term $f(0)$ plus the sum of the sequence shifted by one, i.e., $$\sum_{n \in \mathbb{N}} f(n) = f(0) + \sum_{n \in \mathbb{N}} f(n+1).$$

Cardinal.prod definition

{ι : Type u} (f : ι → Cardinal) : Cardinal

Full source

/-- The indexed product of cardinals is the cardinality of the Pi type
  (dependent product). -/
def prod {ι : Type u} (f : ι → Cardinal) : Cardinal :=
  #(Π i, (f i).out)

Indexed product of cardinals

Informal description

The indexed product of a family of cardinals $\{f(i)\}_{i \in \iota}$ is defined as the cardinality of the dependent product type $\prod_{i \in \iota} \alpha_i$, where each $\alpha_i$ is a representative type of the cardinal $f(i)$. In other words, it represents the cardinality of the collection of all functions that assign to each index $i$ an element of a type with cardinality $f(i)$.

Cardinal.mk_pi theorem

{ι : Type u} (α : ι → Type v) : #(Π i, α i) = prod fun i => #(α i)

Full source

@[simp]
theorem mk_pi {ι : Type u} (α : ι → Type v) : #(Π i, α i) = prod fun i => #(α i) :=
  mk_congr <| Equiv.piCongrRight fun _ => outMkEquiv.symm

Cardinality of Dependent Product Equals Product of Cardinalities

Informal description

For any family of types $\{\alpha_i\}_{i \in \iota}$ indexed by a type $\iota$, the cardinality of the dependent product type $\prod_{i \in \iota} \alpha_i$ is equal to the product of the cardinalities of the individual types $\alpha_i$, i.e., \[ \#\left(\prod_{i \in \iota} \alpha_i\right) = \prod_{i \in \iota} \#\alpha_i. \]

Cardinal.mk_pi_congr_lift theorem

 {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι')
  (h : ∀ i, lift.{w'} #(f i) = lift.{w} #(g (e i))) : lift.{max v' w'} #(Π i, f i) = lift.{max v w} #(Π i, g i)

Full source

theorem mk_pi_congr_lift {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'}
    (e : ι ≃ ι') (h : ∀ i, lift.{w'} #(f i) = lift.{w} #(g (e i))) :
    lift.{max v' w'} #(Π i, f i) = lift.{max v w} #(Π i, g i) :=
  Cardinal.lift_mk_eq'.2 ⟨.piCongr e fun i ↦ Classical.choice <| Cardinal.lift_mk_eq'.1 (h i)⟩

Equality of Lifted Cardinalities of Dependent Products under Index Equivalence

Informal description

Let $\iota$ and $\iota'$ be types in universes $v$ and $v'$ respectively, and let $f : \iota \to \text{Type}_w$ and $g : \iota' \to \text{Type}_{w'}$ be families of types. Given an equivalence $e : \iota \simeq \iota'$ between the index types and a family of equalities $h : \forall i, \text{lift}_{w'} \#(f i) = \text{lift}_w \#(g (e i))$ between the lifted cardinalities of corresponding types, then the lifted cardinalities of the dependent product types satisfy: \[ \text{lift}_{\max(v',w')} \#\left(\prod_{i \in \iota} f i\right) = \text{lift}_{\max(v,w)} \#\left(\prod_{i \in \iota'} g i\right). \]

Cardinal.mk_pi_congr theorem

 {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι') (h : ∀ i, #(f i) = #(g (e i))) :
  #(Π i, f i) = #(Π i, g i)

Full source

theorem mk_pi_congr {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι')
    (h : ∀ i, #(f i) = #(g (e i))) : #(Π i, f i) = #(Π i, g i) :=
  mk_congr <| Equiv.piCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

Cardinality of Dependent Product is Preserved under Index Bijection and Component Cardinality Equality

Informal description

For any types $\iota$ and $\iota'$ in the same universe, and families of types $f : \iota \to \text{Type}_v$ and $g : \iota' \to \text{Type}_v$, if there exists a bijection $e : \iota \simeq \iota'$ such that for each $i \in \iota$, the cardinality of $f(i)$ equals the cardinality of $g(e(i))$, then the cardinality of the dependent product $\prod_{i \in \iota} f(i)$ equals the cardinality of the dependent product $\prod_{i \in \iota'} g(i)$. In symbols: \[ \iota \simeq \iota' \land (\forall i, \#f(i) = \#g(e(i))) \implies \#\left(\prod_{i} f(i)\right) = \#\left(\prod_{i} g(i)\right). \]

Cardinal.mk_pi_congr_prop theorem

 {ι ι' : Prop} {f : ι → Type v} {g : ι' → Type v} (e : ι ↔ ι') (h : ∀ i, #(f i) = #(g (e.mp i))) :
  #(Π i, f i) = #(Π i, g i)

Full source

theorem mk_pi_congr_prop {ι ι' : Prop} {f : ι → Type v} {g : ι' → Type v} (e : ι ↔ ι')
    (h : ∀ i, #(f i) = #(g (e.mp i))) : #(Π i, f i) = #(Π i, g i) :=
  mk_congr <| Equiv.piCongr (.ofIff e) fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

Cardinality Equality of Dependent Products under Propositional Equivalence and Component-wise Cardinality Equality

Informal description

For any propositions $\iota$ and $\iota'$, and families of types $f : \iota \to \text{Type}_v$ and $g : \iota' \to \text{Type}_v$, if there exists a logical equivalence $e : \iota \leftrightarrow \iota'$ such that for every $i : \iota$, the cardinality of $f(i)$ equals the cardinality of $g(e(i))$, then the cardinality of the dependent product $\prod_{i : \iota} f(i)$ equals the cardinality of the dependent product $\prod_{i : \iota'} g(i)$. In symbols: $$\forall \iota \iota' : \text{Prop}, \forall f : \iota \to \text{Type}_v, \forall g : \iota' \to \text{Type}_v, \\ (\exists e : \iota \leftrightarrow \iota', \forall i, \#(f(i)) = \#(g(e(i)))) \implies \#\left(\prod_{i} f(i)\right) = \#\left(\prod_{i} g(i)\right)$$

Cardinal.mk_pi_congr' theorem

 {ι : Type u} {ι' : Type v} {f : ι → Type max w (max u v)} {g : ι' → Type max w (max u v)} (e : ι ≃ ι')
  (h : ∀ i, #(f i) = #(g (e i))) : #(Π i, f i) = #(Π i, g i)

Full source

/-- Similar to `mk_pi_congr` with indexing types in different universes. This is not a strict
generalization. -/
theorem mk_pi_congr' {ι : Type u} {ι' : Type v} {f : ι → Type max w (max u v)}
    {g : ι' → Type max w (max u v)} (e : ι ≃ ι')
    (h : ∀ i, #(f i) = #(g (e i))) : #(Π i, f i) = #(Π i, g i) :=
  mk_congr <| Equiv.piCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

Cardinality of Dependent Products under Index Bijection and Component Cardinality Equality

Informal description

Let $\iota$ and $\iota'$ be types in possibly different universes, and let $f : \iota \to \text{Type}$ and $g : \iota' \to \text{Type}$ be families of types. Given a bijection $e : \iota \simeq \iota'$ and a family of cardinal equalities $h : \forall i, \#(f i) = \#(g (e i))$, the cardinality of the dependent product $\prod_{i} f i$ equals the cardinality of $\prod_{i} g i$.

Cardinal.mk_pi_congrRight theorem

{ι : Type u} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) : #(Π i, f i) = #(Π i, g i)

Full source

theorem mk_pi_congrRight {ι : Type u} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) :
    #(Π i, f i) = #(Π i, g i) :=
  mk_pi_congr (Equiv.refl ι) h

Cardinality Equality of Dependent Products under Component-wise Cardinality Equality

Informal description

For any type $\iota$ and any families of types $f, g : \iota \to \text{Type}_v$, if for every $i \in \iota$ the cardinality of $f(i)$ equals the cardinality of $g(i)$, then the cardinality of the dependent product $\prod_{i \in \iota} f(i)$ equals the cardinality of the dependent product $\prod_{i \in \iota} g(i)$. In symbols: \[ \forall i \in \iota, \#f(i) = \#g(i) \implies \#\left(\prod_{i} f(i)\right) = \#\left(\prod_{i} g(i)\right). \]

Cardinal.mk_pi_congrRight_prop theorem

{ι : Prop} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) : #(Π i, f i) = #(Π i, g i)

Full source

theorem mk_pi_congrRight_prop {ι : Prop} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) :
    #(Π i, f i) = #(Π i, g i) :=
  mk_pi_congr_prop Iff.rfl h

Equality of Dependent Product Cardinalities under Propositional Index and Component-wise Cardinality Equality

Informal description

For any proposition $\iota$ and families of types $f, g : \iota \to \text{Type}_v$, if for every $i : \iota$ the cardinality of $f(i)$ equals the cardinality of $g(i)$, then the cardinality of the dependent product $\prod_{i : \iota} f(i)$ equals the cardinality of $\prod_{i : \iota} g(i)$. In symbols: $$\forall \iota : \text{Prop}, \forall f, g : \iota \to \text{Type}_v, \\ (\forall i, \#(f(i)) = \#(g(i))) \implies \#\left(\prod_{i} f(i)\right) = \#\left(\prod_{i} g(i)\right)$$

Cardinal.prod_const theorem

(ι : Type u) (a : Cardinal.{v}) : (prod fun _ : ι => a) = lift.{u} a ^ lift.{v} #ι

Full source

@[simp]
theorem prod_const (ι : Type u) (a : CardinalCardinal.{v}) :
    (prod fun _ : ι => a) = lift.{u} a ^ lift.{v} #ι :=
  inductionOn a fun _ =>
    mk_congr <| Equiv.piCongr Equiv.ulift.symm fun _ => outMkEquiv.trans Equiv.ulift.symm

Product of Constant Cardinals Equals Lifted Exponentiation: $\prod_{i \in \iota} a = (\text{lift} a)^{\text{lift} \#\iota}$

Informal description

For any type $\iota$ in universe $u$ and any cardinal number $a$ in universe $v$, the product of the constant family of cardinals where each term is $a$ (indexed by $\iota$) is equal to the cardinal exponentiation of the lifted versions: \[ \prod_{i \in \iota} a = (\text{lift}_{u} a)^{\text{lift}_{v} \#\iota}, \] where $\text{lift}_{u}$ and $\text{lift}_{v}$ denote the operations that lift cardinals to higher universes.

Cardinal.prod_const' theorem

(ι : Type u) (a : Cardinal.{u}) : (prod fun _ : ι => a) = a ^ #ι

Full source

theorem prod_const' (ι : Type u) (a : CardinalCardinal.{u}) : (prod fun _ : ι => a) = a ^ #ι :=
  inductionOn a fun _ => (mk_pi _).symm

Product of Constant Cardinals Equals Cardinal Exponentiation: $\prod_{i \in \iota} a = a^{\#\iota}$

Informal description

For any type $\iota$ and any cardinal number $a$ in the same universe, the product of the constant family of cardinals where each term is $a$ (indexed by $\iota$) is equal to $a$ raised to the power of the cardinality of $\iota$, i.e., \[ \prod_{i \in \iota} a = a^{\#\iota}. \]

Cardinal.prod_eq_zero theorem

{ι} (f : ι → Cardinal.{u}) : prod f = 0 ↔ ∃ i, f i = 0

Full source

@[simp]
theorem prod_eq_zero {ι} (f : ι → CardinalCardinal.{u}) : prodprod f = 0 ↔ ∃ i, f i = 0 := by
  lift f to ι → Type u using fun _ => trivial
  simp only [mk_eq_zero_iff, ← mk_pi, isEmpty_pi]

Vanishing of Indexed Product of Cardinals: $\prod_{i \in \iota} f(i) = 0 \leftrightarrow \exists i, f(i) = 0$

Informal description

For any family of cardinal numbers $\{f(i)\}_{i \in \iota}$, the product $\prod_{i \in \iota} f(i)$ equals zero if and only if there exists an index $i$ such that $f(i) = 0$.

Cardinal.prod_ne_zero theorem

{ι} (f : ι → Cardinal) : prod f ≠ 0 ↔ ∀ i, f i ≠ 0

Full source

theorem prod_ne_zero {ι} (f : ι → Cardinal) : prodprod f ≠ 0prod f ≠ 0 ↔ ∀ i, f i ≠ 0 := by simp [prod_eq_zero]

Nonzero Product of Cardinals if and only if All Factors are Nonzero

Informal description

For any family of cardinal numbers $\{f_i\}_{i \in \iota}$, the product $\prod_{i \in \iota} f_i$ is nonzero if and only if $f_i \neq 0$ for every index $i \in \iota$.

Cardinal.power_sum theorem

{ι} (a : Cardinal) (f : ι → Cardinal) : a ^ sum f = prod fun i ↦ a ^ f i

Full source

theorem power_sum {ι} (a : Cardinal) (f : ι → Cardinal) :
    a ^ sum f = prod fun i ↦ a ^ f i := by
  induction a using Cardinal.inductionOn with | _ α =>
  induction f using induction_on_pi with | _ f =>
  simp_rw [prod, sum, power_def]
  apply mk_congr
  refine (Equiv.piCurry fun _ _ => α).trans ?_
  refine Equiv.piCongrRight fun b => ?_
  refine (Equiv.arrowCongr outMkEquiv (Equiv.refl α)).trans ?_
  exact outMkEquiv.symm

Exponentiation of Sum Equals Product of Exponentials in Cardinal Arithmetic

Informal description

For any cardinal number $a$ and any family of cardinals $(f_i)_{i \in \iota}$, the exponentiation $a^{\sum_{i \in \iota} f_i}$ is equal to the product $\prod_{i \in \iota} a^{f_i}$.

Cardinal.lift_prod theorem

{ι : Type u} (c : ι → Cardinal.{v}) : lift.{w} (prod c) = prod fun i => lift.{w} (c i)

Full source

@[simp]
theorem lift_prod {ι : Type u} (c : ι → CardinalCardinal.{v}) :
    lift.{w} (prod c) = prod fun i => lift.{w} (c i) := by
  lift c to ι → Type v using fun _ => trivial
  simp only [← mk_pi, ← mk_uLift]
  exact mk_congr (Equiv.ulift.trans <| Equiv.piCongrRight fun i => Equiv.ulift.symm)

Lift Commutes with Cardinal Product: $\text{lift}_{w} \left( \prod_{i} c_i \right) = \prod_{i} \text{lift}_{w}(c_i)$

Informal description

For any family of cardinal numbers $\{c_i\}_{i \in \iota}$ indexed by a type $\iota$ in universe `Type u`, the lift of their product to a higher universe `Type w` is equal to the product of the lifts of each individual cardinal $c_i$ to the same universe. That is, \[ \text{lift}_{w} \left( \prod_{i \in \iota} c_i \right) = \prod_{i \in \iota} \text{lift}_{w}(c_i). \]

Cardinal.aleph0 definition

: Cardinal.{u}

Full source

/-- `ℵ₀` is the smallest infinite cardinal. -/
def aleph0 : CardinalCardinal.{u} :=
  lift #ℕ

Aleph-null (the first infinite cardinal)

Informal description

The cardinal number $\aleph_0$ is the smallest infinite cardinal, defined as the cardinality of the set of natural numbers $\mathbb{N}$ (lifted to the appropriate universe level).

Cardinal.termℵ₀ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped notation "ℵ₀" => Cardinal.aleph0

Aleph-null (ℵ₀) - the first infinite cardinal

Informal description

The notation `ℵ₀` represents the first infinite cardinal number, which is the cardinality of the set of natural numbers ℕ. This notation is universe-polymorphic, meaning it can be used in any universe level while maintaining its mathematical meaning as the smallest infinite cardinal.

Cardinal.mk_nat theorem

: #ℕ = ℵ₀

Full source

theorem mk_nat : #ℕ = ℵ₀ :=
  (lift_id _).symm

Cardinality of Natural Numbers Equals Aleph-null: $\#\mathbb{N} = \aleph_0$

Informal description

The cardinality of the set of natural numbers $\mathbb{N}$ is equal to $\aleph_0$, i.e., $\#\mathbb{N} = \aleph_0$.

Cardinal.aleph0_ne_zero theorem

: ℵ₀ ≠ 0

Full source

theorem aleph0_ne_zero : ℵ₀ℵ₀ ≠ 0 :=
  mk_ne_zero _

Nonzero Property of Aleph-null: $\aleph_0 \neq 0$

Informal description

The first infinite cardinal $\aleph_0$ is not equal to zero, i.e., $\aleph_0 \neq 0$.

Cardinal.lift_aleph0 theorem

: lift ℵ₀ = ℵ₀

Full source

@[simp]
theorem lift_aleph0 : lift ℵ₀ = ℵ₀ :=
  lift_lift _

Lift Invariance of Aleph-null: $\text{lift}(\aleph_0) = \aleph_0$

Informal description

The lift operation applied to the cardinal $\aleph_0$ (the cardinality of the natural numbers) preserves its value, i.e., $\text{lift}(\aleph_0) = \aleph_0$.

Cardinal.lift_mk_fin theorem

(n : ℕ) : lift #(Fin n) = n

Full source

theorem lift_mk_fin (n : ℕ) : lift #(Fin n) = n := rfl

Lift of Cardinality of Finite Type Equals Natural Number: $\text{lift}(\#(\text{Fin}(n))) = n$

Informal description

For any natural number $n$, the lift of the cardinality of the finite type $\text{Fin}(n)$ (the type with $n$ elements) is equal to $n$ as a cardinal number. That is, $\text{lift}(\#(\text{Fin}(n))) = n$.

Cardinal.mk_empty theorem

: #Empty = 0

Full source

theorem mk_empty : #Empty = 0 :=
  mk_eq_zero _

Cardinality of Empty Type is Zero

Informal description

The cardinality of the empty type $\text{Empty}$ is equal to $0$, i.e., $\#\text{Empty} = 0$.

Cardinal.mk_pempty theorem

: #PEmpty = 0

Full source

theorem mk_pempty : #PEmpty = 0 :=
  mk_eq_zero _

Cardinality of Empty Type is Zero

Informal description

The cardinality of the empty type `PEmpty` is equal to $0$, i.e., $\#\text{PEmpty} = 0$.

Cardinal.mk_punit theorem

: #PUnit = 1

Full source

theorem mk_punit : #PUnit = 1 :=
  mk_eq_one PUnit

Cardinality of PUnit is One

Informal description

The cardinality of the type `PUnit` (the type with exactly one term) is equal to $1$, i.e., $\#\text{PUnit} = 1$.

Cardinal.mk_unit theorem

: #Unit = 1

Full source

theorem mk_unit : #Unit = 1 :=
  mk_punit

Cardinality of Unit Type is One

Informal description

The cardinality of the type `Unit` (the type with exactly one term) is equal to $1$, i.e., $\#\text{Unit} = 1$.

Cardinal.mk_plift_true theorem

: #(PLift True) = 1

Full source

theorem mk_plift_true : #(PLift True) = 1 :=
  mk_eq_one _

Cardinality of Lifted True Type is One

Informal description

The cardinality of the lifted type $\mathrm{PLift}\,\text{True}$ is equal to $1$, i.e., $\#(\mathrm{PLift}\,\text{True}) = 1$.

Cardinal.mk_plift_false theorem

: #(PLift False) = 0

Full source

theorem mk_plift_false : #(PLift False) = 0 :=
  mk_eq_zero _

Cardinality of Lifted Empty Type is Zero

Informal description

The cardinality of the lifted empty type $\mathrm{PLift}\,\text{False}$ is equal to $0$, i.e., $\#(\mathrm{PLift}\,\text{False}) = 0$.

Cardinal.mk_subtype_of_equiv theorem

{α β : Type u} (p : β → Prop) (e : α ≃ β) : #{ a : α // p (e a) } = #{ b : β // p b }

Full source

theorem mk_subtype_of_equiv {α β : Type u} (p : β → Prop) (e : α ≃ β) :
    #{ a : α // p (e a) } = #{ b : β // p b } :=
  mk_congr (Equiv.subtypeEquivOfSubtype e)

Cardinality Preservation of Subtypes under Bijection

Informal description

Given types $\alpha$ and $\beta$ in the same universe, a predicate $p : \beta \to \text{Prop}$, and a bijection $e : \alpha \simeq \beta$, the cardinality of the subtype $\{a \in \alpha \mid p(e(a))\}$ is equal to the cardinality of the subtype $\{b \in \beta \mid p(b)\}$.

Mathlib.SetTheory.Cardinal.Defs

Main definitions

Implementation notes

References

Tags