Mathlib.SetTheory.Cardinal.Order

Cardinal.instLE instance

: LE Cardinal.{u}

Full source

/-- We define the order on cardinal numbers by `#α ≤ #β` if and only if
  there exists an embedding (injective function) from α to β. -/
instance : LE CardinalCardinal.{u} :=
  ⟨fun q₁ q₂ =>
    Quotient.liftOn₂ q₁ q₂ (fun α β => Nonempty <| α ↪ β) fun _ _ _ _ ⟨e₁⟩ ⟨e₂⟩ =>
      propext ⟨fun ⟨e⟩ => ⟨e.congr e₁ e₂⟩, fun ⟨e⟩ => ⟨e.congr e₁.symm e₂.symm⟩⟩⟩

Order on Cardinal Numbers via Embeddings

Informal description

For any two cardinal numbers $\#\alpha$ and $\#\beta$, we say $\#\alpha \leq \#\beta$ if and only if there exists an injective function from $\alpha$ to $\beta$.

Cardinal.partialOrder instance

: PartialOrder Cardinal.{u}

Full source

instance partialOrder : PartialOrder CardinalCardinal.{u} where
  le := (· ≤ ·)
  le_refl := by
    rintro ⟨α⟩
    exact ⟨Embedding.refl _⟩
  le_trans := by
    rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨e₁⟩ ⟨e₂⟩
    exact ⟨e₁.trans e₂⟩
  le_antisymm := by
    rintro ⟨α⟩ ⟨β⟩ ⟨e₁⟩ ⟨e₂⟩
    exact Quotient.sound (e₁.antisymm e₂)

Partial Order on Cardinal Numbers via Injections

Informal description

The cardinal numbers form a partial order, where the order relation $\leq$ is defined by the existence of an injective function between the corresponding types. That is, for any two cardinal numbers $\#\alpha$ and $\#\beta$, we have $\#\alpha \leq \#\beta$ if and only if there exists an injective function from $\alpha$ to $\beta$.

Cardinal.linearOrder instance

: LinearOrder Cardinal.{u}

Full source

instance linearOrder : LinearOrder CardinalCardinal.{u} :=
  { Cardinal.partialOrder with
    le_total := by
      rintro ⟨α⟩ ⟨β⟩
      apply Embedding.total
    toDecidableLE := Classical.decRel _ }

Linear Order on Cardinal Numbers via Injections

Informal description

The cardinal numbers form a linear order, where the order relation $\leq$ is defined by the existence of an injective function between the corresponding types. That is, for any two cardinal numbers $\#\alpha$ and $\#\beta$, we have $\#\alpha \leq \#\beta$ if and only if there exists an injective function from $\alpha$ to $\beta$, and this order is total.

Cardinal.le_def theorem

(α β : Type u) : #α ≤ #β ↔ Nonempty (α ↪ β)

Full source

theorem le_def (α β : Type u) : #α#α ≤ #β ↔ Nonempty (α ↪ β) :=
  Iff.rfl

Cardinal Order via Injections: $\#\alpha \leq \#\beta \leftrightarrow \exists f: \alpha \hookrightarrow \beta$

Informal description

For any two types $\alpha$ and $\beta$ in the same universe, the cardinality $\#\alpha$ is less than or equal to the cardinality $\#\beta$ if and only if there exists an injective function from $\alpha$ to $\beta$.

Cardinal.mk_le_of_injective theorem

{α β : Type u} {f : α → β} (hf : Injective f) : #α ≤ #β

Full source

theorem mk_le_of_injective {α β : Type u} {f : α → β} (hf : Injective f) : #α ≤ #β :=
  ⟨⟨f, hf⟩⟩

Cardinality Comparison via Injective Functions: $\#\alpha \leq \#\beta$ if $\alpha$ injects into $\beta$

Informal description

For any types $\alpha$ and $\beta$ in the same universe, if there exists an injective function $f: \alpha \to \beta$, then the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$, i.e., $\#\alpha \leq \#\beta$.

Function.Embedding.cardinal_le theorem

{α β : Type u} (f : α ↪ β) : #α ≤ #β

Full source

theorem _root_.Function.Embedding.cardinal_le {α β : Type u} (f : α ↪ β) : #α ≤ #β :=
  ⟨f⟩

Cardinality Comparison via Injective Functions: $\#\alpha \leq \#\beta$ if $\alpha \hookrightarrow \beta$

Informal description

For any types $\alpha$ and $\beta$ in the same universe, if there exists an injective function $f: \alpha \hookrightarrow \beta$, then the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$, i.e., $\#\alpha \leq \#\beta$.

Cardinal.mk_le_of_surjective theorem

{α β : Type u} {f : α → β} (hf : Surjective f) : #β ≤ #α

Full source

theorem mk_le_of_surjective {α β : Type u} {f : α → β} (hf : Surjective f) : #β ≤ #α :=
  ⟨Embedding.ofSurjective f hf⟩

Cardinality Comparison via Surjective Functions: $\#\beta \leq \#\alpha$ if $\alpha$ surjects onto $\beta$

Informal description

For any types $\alpha$ and $\beta$ in the same universe, if there exists a surjective function $f: \alpha \to \beta$, then the cardinality of $\beta$ is less than or equal to the cardinality of $\alpha$, i.e., $\#\beta \leq \#\alpha$.

Cardinal.le_mk_iff_exists_set theorem

{c : Cardinal} {α : Type u} : c ≤ #α ↔ ∃ p : Set α, #p = c

Full source

theorem le_mk_iff_exists_set {c : Cardinal} {α : Type u} : c ≤ #α ↔ ∃ p : Set α, #p = c :=
  ⟨inductionOn c fun _ ⟨⟨f, hf⟩⟩ => ⟨Set.range f, (Equiv.ofInjective f hf).cardinal_eq.symm⟩,
    fun ⟨_, e⟩ => e ▸ ⟨⟨Subtype.val, fun _ _ => Subtype.eq⟩⟩⟩

Cardinal Inequality via Subset Existence: $c \leq \#\alpha \iff \exists p \subseteq \alpha, \#p = c$

Informal description

For any cardinal number $c$ and any type $\alpha$, the inequality $c \leq \#\alpha$ holds if and only if there exists a subset $p \subseteq \alpha$ such that the cardinality of $p$ is equal to $c$.

Cardinal.mk_subtype_le theorem

{α : Type u} (p : α → Prop) : #(Subtype p) ≤ #α

Full source

theorem mk_subtype_le {α : Type u} (p : α → Prop) : #(Subtype p) ≤ #α :=
  ⟨Embedding.subtype p⟩

Cardinality of Subtype is Bounded by Original Type

Informal description

For any type $\alpha$ and predicate $p : \alpha \to \text{Prop}$, the cardinality of the subtype $\{x \in \alpha \mid p(x)\}$ is less than or equal to the cardinality of $\alpha$, i.e., $\#\{x \in \alpha \mid p(x)\} \leq \#\alpha$.

Cardinal.mk_set_le theorem

(s : Set α) : #s ≤ #α

Full source

theorem mk_set_le (s : Set α) : #s ≤ #α :=
  mk_subtype_le s

Cardinality of Subset is Bounded by Original Type

Informal description

For any set $s$ over a type $\alpha$, the cardinality of $s$ is less than or equal to the cardinality of $\alpha$, i.e., $\#s \leq \#\alpha$.

Cardinal.out_embedding theorem

{c c' : Cardinal} : c ≤ c' ↔ Nonempty (c.out ↪ c'.out)

Full source

theorem out_embedding {c c' : Cardinal} : c ≤ c' ↔ Nonempty (c.out ↪ c'.out) := by
  conv_lhs => rw [← Cardinal.mk_out c, ← Cardinal.mk_out c', le_def]

Cardinal Order via Representative Injections: $c \leq c' \leftrightarrow \exists f: c.\mathrm{out} \hookrightarrow c'.\mathrm{out}$

Informal description

For any two cardinal numbers $c$ and $c'$, the inequality $c \leq c'$ holds if and only if there exists an injective function from the representative type of $c$ to the representative type of $c'$.

Cardinal.lift_mk_le theorem

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

Full source

theorem lift_mk_le {α : Type v} {β : Type w} :
    liftlift.{max u w} #α ≤ lift.{max u v} #β ↔ Nonempty (α ↪ β) :=
  ⟨fun ⟨f⟩ => ⟨Embedding.congr Equiv.ulift Equiv.ulift f⟩, fun ⟨f⟩ =>
    ⟨Embedding.congr Equiv.ulift.symm Equiv.ulift.symm f⟩⟩

Lifted Cardinal Inequality via Injections: $\mathrm{lift} \#\alpha \leq \mathrm{lift} \#\beta \leftrightarrow \alpha \hookrightarrow \beta$

Informal description

For any types $\alpha$ in universe `Type v` and $\beta$ in universe `Type w`, the inequality $\mathrm{lift}_{\max(u,w)} \#\alpha \leq \mathrm{lift}_{\max(u,v)} \#\beta$ holds if and only if there exists an injective function from $\alpha$ to $\beta$.

Cardinal.lift_mk_le' theorem

{α : Type u} {β : Type v} : lift.{v} #α ≤ lift.{u} #β ↔ Nonempty (α ↪ β)

Full source

/-- A variant of `Cardinal.lift_mk_le` 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_le' {α : Type u} {β : Type v} : liftlift.{v} #α ≤ lift.{u} #β ↔ Nonempty (α ↪ β) :=
  lift_mk_le.{0}

Lifted Cardinal Inequality via Injections: $\mathrm{lift} \#\alpha \leq \mathrm{lift} \#\beta \leftrightarrow \alpha \hookrightarrow \beta$

Informal description

For any types $\alpha$ in universe `Type u` and $\beta$ in universe `Type v`, the inequality $\mathrm{lift}_{v} \#\alpha \leq \mathrm{lift}_{u} \#\beta$ holds if and only if there exists an injective function from $\alpha$ to $\beta$.

Cardinal.liftInitialSeg definition

: Cardinal.{u} ≤i Cardinal.{max u v}

Full source

/-- `Cardinal.lift` as an `InitialSeg`. -/
@[simps!]
def liftInitialSeg : CardinalCardinal.{u}Cardinal.{u} ≤i Cardinal.{max u v} := by
  refine ⟨(OrderEmbedding.ofMapLEIff lift ?_).ltEmbedding, ?_⟩ <;> intro a b
  · refine inductionOn₂ a b fun _ _ ↦ ?_
    rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]
  · refine inductionOn₂ a b fun α β h ↦ ?_
    obtain ⟨e⟩ := h.le
    replace e := e.congr (Equiv.refl β) Equiv.ulift
    refine ⟨#(range e), mk_congr (Equiv.ulift.trans <| Equiv.symm ?_)⟩
    apply (e.codRestrict _ mem_range_self).equivOfSurjective
    rintro ⟨a, ⟨b, rfl⟩⟩
    exact ⟨b, rfl⟩

Initial segment embedding induced by cardinal lift

Informal description

The function `Cardinal.lift` induces an initial segment embedding from the cardinals in universe `Type u` to the cardinals in universe `Type (max u v)`. This means that for any cardinals `a` and `b` in `Type u`, `a ≤ b` if and only if `lift a ≤ lift b` in `Type (max u v)`, and the range of `lift` forms a lower set in the cardinals of `Type (max u v)`.

Cardinal.mem_range_lift_of_le theorem

{a : Cardinal.{u}} {b : Cardinal.{max u v}} : b ≤ lift.{v, u} a → b ∈ Set.range lift.{v, u}

Full source

theorem mem_range_lift_of_le {a : CardinalCardinal.{u}} {b : CardinalCardinal.{max u v}} :
    b ≤ lift.{v, u} a → b ∈ Set.range lift.{v, u} :=
  liftInitialSeg.mem_range_of_le

Range Membership of Cardinal Lift under Inequality

Informal description

For any cardinal number $a$ in universe `Type u` and any cardinal number $b$ in universe `Type (max u v)`, if $b \leq \text{lift}_{v,u}(a)$, then $b$ is in the range of the lift function $\text{lift}_{v,u} \colon \text{Cardinal.{u}} \to \text{Cardinal.{max u v}}$.

Cardinal.lift_injective theorem

: Injective lift.{u, v}

Full source

theorem lift_injective : Injective liftlift.{u, v} :=
  liftInitialSeg.injective

Injectivity of Cardinal Lift Operation

Informal description

The lift operation on cardinal numbers, which maps a cardinal $c$ in universe `Type u` to a cardinal in universe `Type (max u v)`, is injective. That is, for any two cardinals $a$ and $b$ in `Type u$, if $\text{lift}(a) = \text{lift}(b)$, then $a = b$.

Cardinal.lift_inj theorem

{a b : Cardinal.{u}} : lift.{v, u} a = lift.{v, u} b ↔ a = b

Full source

@[simp]
theorem lift_inj {a b : CardinalCardinal.{u}} : liftlift.{v, u} a = lift.{v, u} b ↔ a = b :=
  lift_injective.eq_iff

Lift Operation on Cardinals is Injective: $\text{lift}(a) = \text{lift}(b) \leftrightarrow a = b$

Informal description

For any two cardinal numbers $a$ and $b$ in universe `Type u`, the lift of $a$ to universe `Type (max u v)` is equal to the lift of $b$ if and only if $a = b$ in the original universe.

Cardinal.lift_le theorem

{a b : Cardinal.{v}} : lift.{u} a ≤ lift.{u} b ↔ a ≤ b

Full source

@[simp]
theorem lift_le {a b : CardinalCardinal.{v}} : liftlift.{u} a ≤ lift.{u} b ↔ a ≤ b :=
  liftInitialSeg.le_iff_le

Lift Preserves Cardinal Order: $\text{lift}(a) \leq \text{lift}(b) \leftrightarrow a \leq b$

Informal description

For any two cardinal numbers $a$ and $b$ in universe `Type v`, the lift of $a$ to universe `Type (max u v)` is less than or equal to the lift of $b$ if and only if $a \leq b$ in the original universe.

Cardinal.lift_lt theorem

{a b : Cardinal.{u}} : lift.{v, u} a < lift.{v, u} b ↔ a < b

Full source

@[simp]
theorem lift_lt {a b : CardinalCardinal.{u}} : liftlift.{v, u} a < lift.{v, u} b ↔ a < b :=
  liftInitialSeg.lt_iff_lt

Preservation of Strict Order under Cardinal Lift: $\text{lift}_{v,u}(a) < \text{lift}_{v,u}(b) \leftrightarrow a < b$

Informal description

For any two cardinal numbers $a$ and $b$ in universe `Type u`, the lift of $a$ to universe `Type (max u v)` is strictly less than the lift of $b$ if and only if $a$ is strictly less than $b$ in the original universe.

Cardinal.lift_strictMono theorem

: StrictMono lift

Full source

theorem lift_strictMono : StrictMono lift := fun _ _ => lift_lt.2

Strict Monotonicity of Cardinal Lift: $a < b \Rightarrow \text{lift}(a) < \text{lift}(b)$

Informal description

The function $\text{lift} : \text{Cardinal} \to \text{Cardinal}$ is strictly monotone, meaning that for any two cardinal numbers $a$ and $b$, if $a < b$ then $\text{lift}(a) < \text{lift}(b)$.

Cardinal.lift_monotone theorem

: Monotone lift

Full source

theorem lift_monotone : Monotone lift :=
  lift_strictMono.monotone

Monotonicity of Cardinal Lift: $a \leq b \Rightarrow \text{lift}(a) \leq \text{lift}(b)$

Informal description

The function $\text{lift} : \text{Cardinal} \to \text{Cardinal}$ is monotone, meaning that for any two cardinal numbers $a$ and $b$, if $a \leq b$ then $\text{lift}(a) \leq \text{lift}(b)$.

Cardinal.lift_min theorem

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

Full source

@[simp]
theorem lift_min {a b : Cardinal} : lift.{u, v} (min a b) = min (lift.{u, v} a) (lift.{u, v} b) :=
  lift_monotone.map_min

Lift Preserves Minimum of Cardinals: $\text{lift}(\min(a, b)) = \min(\text{lift}(a), \text{lift}(b))$

Informal description

For any two cardinal numbers $a$ and $b$, the lift of their minimum equals the minimum of their lifts. That is, $\text{lift}(\min(a, b)) = \min(\text{lift}(a), \text{lift}(b))$.

Cardinal.lift_max theorem

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

Full source

@[simp]
theorem lift_max {a b : Cardinal} : lift.{u, v} (max a b) = max (lift.{u, v} a) (lift.{u, v} b) :=
  lift_monotone.map_max

Lift Preserves Maximum of Cardinals: $\text{lift}(\max(a, b)) = \max(\text{lift}(a), \text{lift}(b))$

Informal description

For any two cardinal numbers $a$ and $b$, the lift of their maximum equals the maximum of their lifts. That is, $\text{lift}(\max(a, b)) = \max(\text{lift}(a), \text{lift}(b))$.

Cardinal.lift_umax_eq theorem

{a : Cardinal.{u}} {b : Cardinal.{v}} : lift.{max v w} a = lift.{max u w} b ↔ lift.{v} a = lift.{u} b

Full source

theorem lift_umax_eq {a : CardinalCardinal.{u}} {b : CardinalCardinal.{v}} :
    liftlift.{max v w} a = lift.{max u w} b ↔ lift.{v} a = lift.{u} b := by
  rw [← lift_lift.{v, w, u}, ← lift_lift.{u, w, v}, lift_inj]

Equality of Lifted Cardinals Across Universes: $\text{lift}_{\max(v,w)}(a) = \text{lift}_{\max(u,w)}(b) \leftrightarrow \text{lift}_v(a) = \text{lift}_u(b)$

Informal description

For any cardinal numbers $a$ in universe `Type u` and $b$ in universe `Type v`, the lift of $a$ to universe `Type (max v w)` equals the lift of $b$ to universe `Type (max u w)$ if and only if the lift of $a$ to universe `Type v` equals the lift of $b$ to universe `Type u$. In other words, the following equivalence holds: $$\text{lift}_{\max(v,w)}(a) = \text{lift}_{\max(u,w)}(b) \leftrightarrow \text{lift}_v(a) = \text{lift}_u(b).$$

Cardinal.le_lift_iff theorem

{a : Cardinal.{u}} {b : Cardinal.{max u v}} : b ≤ lift.{v, u} a ↔ ∃ a' ≤ a, lift.{v, u} a' = b

Full source

theorem le_lift_iff {a : CardinalCardinal.{u}} {b : CardinalCardinal.{max u v}} :
    b ≤ lift.{v, u} a ↔ ∃ a' ≤ a, lift.{v, u} a' = b :=
  liftInitialSeg.le_apply_iff

Characterization of Cardinal Inequality under Universe Lifting: $b \leq \text{lift}(a) \leftrightarrow \exists a' \leq a, \text{lift}(a') = b$

Informal description

For any cardinal number $a$ in universe $u$ and $b$ in universe $\max(u,v)$, we have $b \leq \text{lift}_{v,u}(a)$ if and only if there exists a cardinal $a' \leq a$ in universe $u$ such that $\text{lift}_{v,u}(a') = b$.

Cardinal.lt_lift_iff theorem

{a : Cardinal.{u}} {b : Cardinal.{max u v}} : b < lift.{v, u} a ↔ ∃ a' < a, lift.{v, u} a' = b

Full source

theorem lt_lift_iff {a : CardinalCardinal.{u}} {b : CardinalCardinal.{max u v}} :
    b < lift.{v, u} a ↔ ∃ a' < a, lift.{v, u} a' = b :=
  liftInitialSeg.lt_apply_iff

Characterization of Elements Below Lifted Cardinal

Informal description

For any cardinal numbers $a$ in universe `Type u` and $b$ in universe `Type (max u v)`, the inequality $b < \text{lift}_{v, u} a$ holds if and only if there exists a cardinal $a' < a$ in `Type u` such that $\text{lift}_{v, u} a' = b$.

Cardinal.lift_eq_zero theorem

{a : Cardinal.{v}} : lift.{u} a = 0 ↔ a = 0

Full source

@[simp]
theorem lift_eq_zero {a : CardinalCardinal.{v}} : liftlift.{u} a = 0 ↔ a = 0 :=
  lift_injective.eq_iff' lift_zero

Lift of Cardinal is Zero if and only if Cardinal is Zero

Informal description

For any cardinal number $a$ in universe `Type v`, the lift of $a$ to a higher universe is zero if and only if $a$ itself is zero, i.e., $\text{lift}_{u}(a) = 0 \leftrightarrow a = 0$.

Cardinal.mk_fintype theorem

(α : Type u) [h : Fintype α] : #α = Fintype.card α

Full source

@[simp]
theorem mk_fintype (α : Type u) [h : Fintype α] : #α = Fintype.card α :=
  mk_congr (Fintype.equivOfCardEq (by simp))

Cardinality of Finite Type Equals Its Size

Informal description

For any finite type $\alpha$ (i.e., $\alpha$ has a `Fintype` instance), the cardinality of $\alpha$ is equal to the number of elements in $\alpha$ as given by `Fintype.card`.

Cardinal.commSemiring instance

: CommSemiring Cardinal.{u}

Full source

instance commSemiring : CommSemiring CardinalCardinal.{u} where
  zero := 0
  one := 1
  add := (· + ·)
  mul := (· * ·)
  zero_add a := inductionOn a fun α => mk_congr <| Equiv.emptySum _ α
  add_zero a := inductionOn a fun α => mk_congr <| Equiv.sumEmpty α _
  add_assoc a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumAssoc α β γ
  add_comm a b := inductionOn₂ a b fun α β => mk_congr <| Equiv.sumComm α β
  zero_mul a := inductionOn a fun _ => mk_eq_zero _
  mul_zero a := inductionOn a fun _ => mk_eq_zero _
  one_mul a := inductionOn a fun α => mk_congr <| Equiv.uniqueProd α _
  mul_one a := inductionOn a fun α => mk_congr <| Equiv.prodUnique α _
  mul_assoc a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.prodAssoc α β γ
  mul_comm a b := inductionOn₂ a b fun α β => mk_congr <| Equiv.prodComm α β
  left_distrib a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.prodSumDistrib α β γ
  right_distrib a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumProdDistrib α β γ
  nsmul := nsmulRec
  npow n c := c ^ (n : Cardinal)
  npow_zero := power_zero
  npow_succ n c := by rw [cast_succ, power_add, power_one]
  natCast n := lift #(Fin n)
  natCast_zero := rfl
  natCast_succ n := cast_succ n

Cardinal Numbers Form a Commutative Semiring

Informal description

The type of cardinal numbers $\text{Cardinal}$ forms a commutative semiring, where the addition and multiplication operations are defined via the sum type and product type cardinalities respectively, and the natural numbers embed into the cardinals via their finite cardinalities.

Cardinal.mk_bool theorem

: #Bool = 2

Full source

theorem mk_bool : #Bool = 2 := by simp

Cardinality of Boolean Type: $\#\text{Bool} = 2$

Informal description

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

Cardinal.mk_Prop theorem

: #Prop = 2

Full source

theorem mk_Prop : #Prop = 2 := by simp

Cardinality of Proposition Type is Two

Informal description

The cardinality of the type of propositions `Prop` is equal to 2, i.e., $\#\text{Prop} = 2$.

Cardinal.power_mul theorem

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

Full source

theorem power_mul {a b c : Cardinal} : a ^ (b * c) = (a ^ b) ^ c := by
  rw [mul_comm b c]
  exact inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.curry γ β α

Cardinal exponentiation identity: $a^{b \cdot c} = (a^b)^c$

Informal description

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

Cardinal.power_natCast theorem

(a : Cardinal.{u}) (n : ℕ) : a ^ (↑n : Cardinal.{u}) = a ^ n

Full source

@[simp, norm_cast]
theorem power_natCast (a : CardinalCardinal.{u}) (n : ℕ) : a ^ (↑n : CardinalCardinal.{u}) = a ^ n :=
  rfl

Cardinal Exponentiation of Natural Number Cast: $a^{\overline{n}} = a^n$

Informal description

For any cardinal number $a$ and natural number $n$, the cardinal exponentiation $a^{\overline{n}}$ (where $\overline{n}$ is the embedding of $n$ as a cardinal) is equal to the $n$-fold power $a^n$ in the usual sense.

Cardinal.lift_eq_one theorem

{a : Cardinal.{v}} : lift.{u} a = 1 ↔ a = 1

Full source

@[simp]
theorem lift_eq_one {a : CardinalCardinal.{v}} : liftlift.{u} a = 1 ↔ a = 1 :=
  lift_injective.eq_iff' lift_one

Lift of Cardinal Equals One if and only if Cardinal is One

Informal description

For any cardinal number $a$ in universe `Type v`, the lift of $a$ to universe `Type (max u v)$ is equal to $1$ if and only if $a$ itself is equal to $1$.

Cardinal.lift_mul theorem

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

Full source

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

Lift Preserves Multiplication of Cardinal Numbers

Informal description

For any two cardinal numbers $a$ and $b$ in universe `Type u`, the lift of their product to universe `Type (max u v)` is equal to the product of their lifts, i.e., $\text{lift}(a \cdot b) = \text{lift}(a) \cdot \text{lift}(b)$.

Cardinal.lift_two theorem

: lift.{u, v} 2 = 2

Full source

theorem lift_two : lift.{u, v} 2 = 2 := by simp [← one_add_one_eq_two]

Universe Lift Preserves the Cardinal Two

Informal description

For any universe levels $u$ and $v$, the lift of the cardinal number $2$ from universe `Type u` to universe `Type (max u v)` is equal to $2$.

Cardinal.mk_set theorem

{α : Type u} : #(Set α) = 2 ^ #α

Full source

@[simp]
theorem mk_set {α : Type u} : #(Set α) = 2 ^ #α := by simp [← one_add_one_eq_two, Set, mk_arrow]

Cardinality of Power Set: $\#(\mathcal{P}(\alpha)) = 2^{\#\alpha}$

Informal description

For any type $\alpha$, the cardinality of the set of all subsets of $\alpha$ is equal to $2$ raised to the power of the cardinality of $\alpha$, i.e., $\#(\mathcal{P}(\alpha)) = 2^{\#\alpha}$.

Cardinal.mk_powerset theorem

{α : Type u} (s : Set α) : #(↥(𝒫 s)) = 2 ^ #(↥s)

Full source

/-- A variant of `Cardinal.mk_set` expressed in terms of a `Set` instead of a `Type`. -/
@[simp]
theorem mk_powerset {α : Type u} (s : Set α) : #(↥(𝒫 s)) = 2 ^ #(↥s) :=
  (mk_congr (Equiv.Set.powerset s)).trans mk_set

Cardinality of Powerset: $\#(\mathcal{P}(s)) = 2^{\#s}$

Informal description

For any type $\alpha$ and any subset $s \subseteq \alpha$, the cardinality of the powerset of $s$ (the set of all subsets of $s$) is equal to $2$ raised to the power of the cardinality of $s$, i.e., $\#(\mathcal{P}(s)) = 2^{\#s}$.

Cardinal.lift_two_power theorem

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

Full source

theorem lift_two_power (a : Cardinal) : lift.{v} (2 ^ a) = 2 ^ lift.{v} a := by
  simp [← one_add_one_eq_two]

Lift of Cardinal Power of Two Equals Power of Two of Lift

Informal description

For any cardinal number $a$, the lift of $2^a$ to a higher universe equals $2$ raised to the lift of $a$ in that universe. That is, $\text{lift}(2^a) = 2^{\text{lift}(a)}$.

Cardinal.zero_le theorem

: ∀ a : Cardinal, 0 ≤ a

Full source

protected theorem zero_le : ∀ a : Cardinal, 0 ≤ a := by
  rintro ⟨α⟩
  exact ⟨Embedding.ofIsEmpty⟩

Nonnegativity of Zero Cardinal

Informal description

For any cardinal number $a$, the zero cardinal is less than or equal to $a$, i.e., $0 \leq a$.

Cardinal.addLeftMono instance

: AddLeftMono Cardinal

Full source

instance addLeftMono : AddLeftMono Cardinal :=
  ⟨fun _ _ _ => add_le_add' le_rfl⟩

Monotonicity of Cardinal Addition on the Left

Informal description

For any cardinal number $c$, the function $c + \cdot$ is monotone with respect to the order on cardinals. That is, for any cardinals $a$ and $b$, if $a \leq b$ then $c + a \leq c + b$.

Cardinal.addRightMono instance

: AddRightMono Cardinal

Full source

instance addRightMono : AddRightMono Cardinal :=
  ⟨fun _ _ _ h => add_le_add' h le_rfl⟩

Monotonicity of Cardinal Addition on the Right

Informal description

For any cardinal number $c$, the function $c + \cdot$ is monotone with respect to the order on cardinals. That is, for any cardinals $a$ and $b$, if $a \leq b$ then $c + a \leq c + b$.

Cardinal.canonicallyOrderedAdd instance

: CanonicallyOrderedAdd Cardinal.{u}

Full source

instance canonicallyOrderedAdd : CanonicallyOrderedAdd CardinalCardinal.{u} where
  exists_add_of_le {a b} :=
    inductionOn₂ a b fun α β ⟨⟨f, hf⟩⟩ =>
      have : α ⊕ ((range f)ᶜ : Set β)α ⊕ ((range f)ᶜ : Set β) ≃ β := by
        classical
        exact (Equiv.sumCongr (Equiv.ofInjective f hf) (Equiv.refl _)).trans <|
          Equiv.Set.sumCompl (range f)
      ⟨#(↥(range f)ᶜ), mk_congr this.symm⟩
  le_self_add a _ := (add_zero a).ge.trans <| add_le_add_left (Cardinal.zero_le _) _

Cardinal Numbers Form a Canonically Ordered Additive Monoid

Informal description

The type of cardinal numbers $\text{Cardinal}$ forms a canonically ordered additive monoid, where the order relation $\leq$ is defined by the existence of injective functions between types, and addition corresponds to the cardinality of sum types. This means that for any cardinals $a$ and $b$, $a \leq b$ if and only if there exists a cardinal $c$ such that $b = a + c$.

Cardinal.isOrderedRing instance

: IsOrderedRing Cardinal.{u}

Full source

instance isOrderedRing : IsOrderedRing CardinalCardinal.{u} :=
  CanonicallyOrderedAdd.toIsOrderedRing

Cardinal Numbers Form an Ordered Semiring

Informal description

The cardinal numbers form an ordered semiring, where the order relation $\leq$ is defined by the existence of an injective function between the corresponding types, and the algebraic operations of addition and multiplication correspond to the cardinality of sum types and product types respectively. This means: 1. Addition is monotone (if $a \leq b$ then $a + c \leq b + c$ for all $c$) 2. Multiplication by nonnegative elements is monotone (if $0 \leq a$ and $b \leq c$ then $a \cdot b \leq a \cdot c$) 3. The zero element is less than or equal to the one element ($0 \leq 1$)

Cardinal.orderBot instance

: OrderBot Cardinal.{u}

Full source

instance orderBot : OrderBot CardinalCardinal.{u} := inferInstance

Cardinal Numbers Have a Bottom Element

Informal description

The type of cardinal numbers $\text{Cardinal}$ has a least element $0$ with respect to the order defined by the existence of injective functions between types. That is, for any cardinal number $c$, we have $0 \leq c$.

Cardinal.noZeroDivisors instance

: NoZeroDivisors Cardinal.{u}

Full source

instance noZeroDivisors : NoZeroDivisors CardinalCardinal.{u} where
  eq_zero_or_eq_zero_of_mul_eq_zero := fun {a b} =>
    inductionOn₂ a b fun α β => by
      simpa only [mul_def, mk_eq_zero_iff, isEmpty_prod] using id

Cardinal Numbers Have No Zero Divisors

Informal description

The type of cardinal numbers $\text{Cardinal}$ has no zero divisors, meaning that for any two cardinals $c_1$ and $c_2$, if $c_1 \cdot c_2 = 0$, then either $c_1 = 0$ or $c_2 = 0$.

Cardinal.instLinearOrderedCommMonoidWithZero instance

: LinearOrderedCommMonoidWithZero Cardinal.{u}

Full source

instance : LinearOrderedCommMonoidWithZero CardinalCardinal.{u} :=
  { Cardinal.commSemiring,
    Cardinal.linearOrder with
    bot_le _ := bot_le
    mul_le_mul_left := @mul_le_mul_left' _ _ _ _
    zero_le_one := zero_le _ }

Cardinal Numbers as a Linearly Ordered Commutative Monoid with Zero

Informal description

The cardinal numbers form a linearly ordered commutative monoid with zero, where the order is defined by the existence of injective functions between types, and the multiplication operation corresponds to the cardinality of product types.

Cardinal.instCommMonoidWithZero instance

: CommMonoidWithZero Cardinal.{u}

Full source

instance : CommMonoidWithZero CardinalCardinal.{u} :=
  { Cardinal.commSemiring with }

Cardinal Numbers as a Commutative Monoid with Zero

Informal description

The type of cardinal numbers $\text{Cardinal}$ forms a commutative monoid with zero, where multiplication is commutative and associative with identity element $1$, and $0$ is an absorbing element for multiplication.

Cardinal.instCommMonoid instance

: CommMonoid Cardinal.{u}

Full source

instance : CommMonoid CardinalCardinal.{u} :=
  { Cardinal.commSemiring with }

Cardinal Numbers Form a Commutative Monoid under Multiplication

Informal description

The type of cardinal numbers forms a commutative monoid under multiplication, where the product of two cardinals corresponds to the cardinality of the product type.

Cardinal.zero_power_le theorem

(c : Cardinal.{u}) : (0 : Cardinal.{u}) ^ c ≤ 1

Full source

theorem zero_power_le (c : CardinalCardinal.{u}) : (0 : CardinalCardinal.{u}) ^ c ≤ 1 := by
  by_cases h : c = 0
  · rw [h, power_zero]
  · rw [zero_power h]
    apply zero_le

Inequality for Zero to a Cardinal Power: $0^c \leq 1$

Informal description

For any cardinal number $c$, the zero cardinal raised to the power of $c$ is less than or equal to the one cardinal, i.e., $0^c \leq 1$.

Cardinal.power_le_power_left theorem

: ∀ {a b c : Cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c

Full source

theorem power_le_power_left : ∀ {a b c : Cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c := by
  rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩
  let ⟨a⟩ := mk_ne_zero_iff.1 hα
  exact ⟨@Function.Embedding.arrowCongrLeft _ _ _ ⟨a⟩ e⟩

Monotonicity of Cardinal Exponentiation in the Exponent: $a^b \leq a^c$ when $a \neq 0$ and $b \leq c$

Informal description

For any cardinal numbers $a$, $b$, and $c$, if $a \neq 0$ and $b \leq c$, then $a^b \leq a^c$.

Cardinal.self_le_power theorem

(a : Cardinal) {b : Cardinal} (hb : 1 ≤ b) : a ≤ a ^ b

Full source

theorem self_le_power (a : Cardinal) {b : Cardinal} (hb : 1 ≤ b) : a ≤ a ^ b := by
  rcases eq_or_ne a 0 with (rfl | ha)
  · exact zero_le _
  · convert power_le_power_left ha hb
    exact (power_one a).symm

Cardinal Inequality: $a \leq a^b$ for $1 \leq b$

Informal description

For any cardinal number $a$ and any cardinal number $b$ such that $1 \leq b$, we have $a \leq a^b$.

Cardinal.cantor theorem

(a : Cardinal.{u}) : a < 2 ^ a

Full source

/-- **Cantor's theorem** -/
theorem cantor (a : CardinalCardinal.{u}) : a < 2 ^ a := by
  induction' a using Cardinal.inductionOn with α
  rw [← mk_set]
  refine ⟨⟨⟨singleton, fun a b => singleton_eq_singleton_iff.1⟩⟩, ?_⟩
  rintro ⟨⟨f, hf⟩⟩
  exact cantor_injective f hf

Cantor's Theorem: $a < 2^a$ for any cardinal $a$

Informal description

For any cardinal number $a$, the inequality $a < 2^a$ holds, where $2^a$ denotes the cardinality of the power set of any set with cardinality $a$.

Cardinal.instNoMaxOrder instance

: NoMaxOrder Cardinal.{u}

Full source

instance : NoMaxOrder CardinalCardinal.{u} where exists_gt a := ⟨_, cantor a⟩

No Maximal Cardinal Number

Informal description

The class of cardinal numbers has no maximal element. That is, for any cardinal number $\kappa$, there exists a cardinal number $\lambda$ such that $\kappa < \lambda$.

Cardinal.instDistribLattice instance

: DistribLattice Cardinal.{u}

Full source

instance : DistribLattice CardinalCardinal.{u} := inferInstance

Cardinal Numbers Form a Distributive Lattice

Informal description

The cardinal numbers form a distributive lattice, where the join and meet operations are defined in terms of the order relation given by the existence of injective functions between types.

Cardinal.power_le_max_power_one theorem

{a b c : Cardinal} (h : b ≤ c) : a ^ b ≤ max (a ^ c) 1

Full source

theorem power_le_max_power_one {a b c : Cardinal} (h : b ≤ c) : a ^ b ≤ max (a ^ c) 1 := by
  by_cases ha : a = 0
  · simp [ha, zero_power_le]
  · exact (power_le_power_left ha h).trans (le_max_left _ _)

Upper Bound on Cardinal Exponentiation: $a^b \leq \max(a^c, 1)$ when $b \leq c$

Informal description

For any cardinal numbers $a$, $b$, and $c$, if $b \leq c$, then $a^b \leq \max(a^c, 1)$.

Cardinal.power_le_power_right theorem

{a b c : Cardinal} : a ≤ b → a ^ c ≤ b ^ c

Full source

theorem power_le_power_right {a b c : Cardinal} : a ≤ b → a ^ c ≤ b ^ c :=
  inductionOn₃ a b c fun _ _ _ ⟨e⟩ => ⟨Embedding.arrowCongrRight e⟩

Monotonicity of Cardinal Exponentiation in the Base: $a \leq b \Rightarrow a^c \leq b^c$

Informal description

For any three cardinal numbers $a$, $b$, and $c$, if $a \leq b$, then the exponentiation $a^c$ is less than or equal to $b^c$.

Cardinal.power_pos theorem

{a : Cardinal} (b : Cardinal) (ha : 0 < a) : 0 < a ^ b

Full source

theorem power_pos {a : Cardinal} (b : Cardinal) (ha : 0 < a) : 0 < a ^ b :=
  (power_ne_zero _ ha.ne').bot_lt

Positivity of Cardinal Exponentiation: $0 < a \Rightarrow 0 < a^b$

Informal description

For any cardinal numbers $a$ and $b$, if $0 < a$, then $0 < a^b$.

Cardinal.lt_wf theorem

: @WellFounded Cardinal.{u} (· < ·)

Full source

protected theorem lt_wf : @WellFounded CardinalCardinal.{u} (· < ·) :=
  ⟨fun a =>
    by_contradiction fun h => by
      let ι := { c : Cardinal // ¬Acc (· < ·) c }
      let f : ι → Cardinal := Subtype.val
      haveI hι : Nonempty ι := ⟨⟨_, h⟩⟩
      obtain ⟨⟨c : Cardinal, hc : ¬Acc (· < ·) c⟩, ⟨h_1 : ∀ j, (f ⟨c, hc⟩).out ↪ (f j).out⟩⟩ :=
        Embedding.min_injective fun i => (f i).out
      refine hc (Acc.intro _ fun j h' => by_contradiction fun hj => h'.2 ?_)
      have : #_ ≤ #_ := ⟨h_1 ⟨j, hj⟩⟩
      simpa only [mk_out] using this⟩

Well-foundedness of the Cardinal Ordering

Informal description

The strict less-than relation `<` on cardinal numbers is well-founded. That is, every non-empty collection of cardinals has a minimal element with respect to `<`.

Cardinal.instWellFoundedRelation instance

: WellFoundedRelation Cardinal.{u}

Full source

instance : WellFoundedRelation CardinalCardinal.{u} :=
  ⟨(· < ·), Cardinal.lt_wf⟩

Well-foundedness of the Cardinal Ordering

Informal description

The strict less-than relation $<$ on cardinal numbers is well-founded.

Cardinal.instWellFoundedLT instance

: WellFoundedLT Cardinal.{u}

Full source

instance : WellFoundedLT CardinalCardinal.{u} :=
  ⟨Cardinal.lt_wf⟩

Well-foundedness of the Cardinal Ordering

Informal description

The strict less-than relation `<` on cardinal numbers is well-founded.

Cardinal.instConditionallyCompleteLinearOrderBot instance

: ConditionallyCompleteLinearOrderBot Cardinal

Full source

instance : ConditionallyCompleteLinearOrderBot Cardinal :=
  WellFoundedLT.conditionallyCompleteLinearOrderBot _

Conditionally Complete Linear Order Structure on Cardinal Numbers with Bottom Element

Informal description

The cardinal numbers form a conditionally complete linear order with a bottom element. This means: 1. The order is linear (total) - for any two cardinals $\kappa$ and $\lambda$, either $\kappa \leq \lambda$ or $\lambda \leq \kappa$. 2. Every nonempty set of cardinals that is bounded above has a supremum. 3. Every nonempty set of cardinals has an infimum (automatically bounded below by the bottom element $0$). 4. There exists a least cardinal $0$ (the cardinality of the empty type).

Cardinal.sInf_empty theorem

: sInf (∅ : Set Cardinal.{u}) = 0

Full source

@[simp]
theorem sInf_empty : sInf (∅ : Set CardinalCardinal.{u}) = 0 :=
  dif_neg Set.not_nonempty_empty

Infimum of Empty Set of Cardinals is Zero

Informal description

The infimum of the empty set of cardinal numbers is equal to the zero cardinal, i.e., $\inf \emptyset = 0$.

Cardinal.instSuccOrder instance

: SuccOrder Cardinal

Full source

/-- Note that the successor of `c` is not the same as `c + 1` except in the case of finite `c`. -/
instance : SuccOrder Cardinal := ConditionallyCompleteLinearOrder.toSuccOrder

Successor Order Structure on Cardinal Numbers

Informal description

The cardinal numbers form a successor order, where for each cardinal $\kappa$, the successor $\text{succ}(\kappa)$ is defined as the smallest cardinal strictly greater than $\kappa$. Note that for infinite cardinals, $\text{succ}(\kappa)$ differs from $\kappa + 1$.

Cardinal.succ_def theorem

(c : Cardinal) : succ c = sInf {c' | c < c'}

Full source

theorem succ_def (c : Cardinal) : succ c = sInf { c' | c < c' } :=
  dif_neg <| not_isMax c

Successor Cardinal as Infimum of Larger Cardinals

Informal description

For any cardinal number $c$, the successor cardinal $\text{succ}(c)$ is equal to the infimum of the set of all cardinals $c'$ such that $c < c'$. That is, \[ \text{succ}(c) = \inf \{c' \mid c < c'\}. \]

Cardinal.succ_pos theorem

: ∀ c : Cardinal, 0 < succ c

Full source

theorem succ_pos : ∀ c : Cardinal, 0 < succ c :=
  bot_lt_succ

Successor Cardinals are Positive: $0 < \mathrm{succ}(c)$ for all cardinals $c$

Informal description

For every cardinal number $c$, the successor cardinal $\mathrm{succ}(c)$ is strictly greater than zero.

Cardinal.succ_ne_zero theorem

(c : Cardinal) : succ c ≠ 0

Full source

theorem succ_ne_zero (c : Cardinal) : succsucc c ≠ 0 :=
  (succ_pos _).ne'

Successor Cardinal is Nonzero: $\mathrm{succ}(c) \neq 0$

Informal description

For any cardinal number $c$, the successor cardinal $\mathrm{succ}(c)$ is not equal to zero.

Cardinal.add_one_le_succ theorem

(c : Cardinal.{u}) : c + 1 ≤ succ c

Full source

theorem add_one_le_succ (c : CardinalCardinal.{u}) : c + 1 ≤ succ c := by
  -- Porting note: rewrote the next three lines to avoid defeq abuse.
  have : Set.Nonempty { c' | c < c' } := exists_gt c
  simp_rw [succ_def, le_csInf_iff'' this, mem_setOf]
  intro b hlt
  rcases b, c with ⟨⟨β⟩, ⟨γ⟩⟩
  obtain ⟨f⟩ := le_of_lt hlt
  have : ¬Surjective f := fun hn => (not_le_of_lt hlt) (mk_le_of_surjective hn)
  simp only [Surjective, not_forall] at this
  rcases this with ⟨b, hb⟩
  calc
    #γ + 1 = #(Option γ) := mk_option.symm
    _ ≤ #β := (f.optionElim b hb).cardinal_le

Inequality between Sum and Successor of a Cardinal: $c + 1 \leq \text{succ}(c)$

Informal description

For any cardinal number $c$, the sum $c + 1$ is less than or equal to the successor cardinal $\text{succ}(c)$.

Cardinal.lift_succ theorem

(a) : lift.{v, u} (succ a) = succ (lift.{v, u} a)

Full source

@[simp]
theorem lift_succ (a) : lift.{v, u} (succ a) = succ (lift.{v, u} a) :=
  le_antisymm
    (le_of_not_gt fun h => by
      rcases lt_lift_iff.1 h with ⟨b, h, e⟩
      rw [lt_succ_iff, ← lift_le, e] at h
      exact h.not_lt (lt_succ _))
    (succ_le_of_lt <| lift_lt.2 <| lt_succ a)

Lift Commutes with Successor: $\text{lift}(\text{succ}(a)) = \text{succ}(\text{lift}(a))$

Informal description

For any cardinal number $a$ in universe `Type u`, the lift of the successor of $a$ to universe `Type (max u v)` is equal to the successor of the lift of $a$ to the same universe. In symbols: $$\text{lift}_{v,u}(\text{succ}(a)) = \text{succ}(\text{lift}_{v,u}(a))$$

Cardinal.ne_zero_of_isSuccLimit theorem

{c} (h : IsSuccLimit c) : c ≠ 0

Full source

theorem ne_zero_of_isSuccLimit {c} (h : IsSuccLimit c) : c ≠ 0 :=
  h.ne_bot

Nonzero Property of Successor Limit Cardinals

Informal description

For any cardinal number $c$, if $c$ is a successor limit cardinal, then $c$ is not equal to zero.

Cardinal.isSuccPrelimit_zero theorem

: IsSuccPrelimit (0 : Cardinal)

Full source

theorem isSuccPrelimit_zero : IsSuccPrelimit (0 : Cardinal) :=
  isSuccPrelimit_bot

Zero is a Successor Pre-Limit Cardinal

Informal description

The cardinal number $0$ is a successor pre-limit, meaning there is no cardinal number strictly less than $0$ that is covered by $0$ in the order on cardinals.

Cardinal.isSuccLimit_iff theorem

{c : Cardinal} : IsSuccLimit c ↔ c ≠ 0 ∧ IsSuccPrelimit c

Full source

protected theorem isSuccLimit_iff {c : Cardinal} : IsSuccLimitIsSuccLimit c ↔ c ≠ 0 ∧ IsSuccPrelimit c :=
  isSuccLimit_iff

Characterization of Limit Cardinals: $c$ is a limit cardinal iff $c \neq 0$ and $\forall x < c, \text{succ}(x) < c$

Informal description

A cardinal number $c$ is a (weak) limit cardinal if and only if $c \neq 0$ and for every cardinal $x < c$, the successor of $x$ is also less than $c$ (i.e., $c$ is a successor pre-limit).

Cardinal.IsStrongLimit structure

(c : Cardinal)

Full source

/-- A cardinal is a strong limit if it is not zero and it is closed under powersets.
Note that `ℵ₀` is a strong limit by this definition. -/
structure IsStrongLimit (c : Cardinal) : Prop where
  ne_zero : c ≠ 0
  two_power_lt ⦃x⦄ : x < c → 2 ^ x < c

Strong limit cardinal

Informal description

A cardinal number $ c $ is called a *strong limit cardinal* if it is nonzero and for every cardinal $ x < c $, the power set cardinal $ 2^x $ is also less than $ c $. This includes $ \aleph_0 $ (the cardinality of the natural numbers) as a strong limit cardinal under this definition.

Cardinal.IsStrongLimit.isSuccLimit theorem

{c} (H : IsStrongLimit c) : IsSuccLimit c

Full source

protected theorem IsStrongLimit.isSuccLimit {c} (H : IsStrongLimit c) : IsSuccLimit c := by
  rw [Cardinal.isSuccLimit_iff]
  exact ⟨H.ne_zero, isSuccPrelimit_of_succ_lt fun x h ↦
    (succ_le_of_lt <| cantor x).trans_lt (H.two_power_lt h)⟩

Strong Limit Cardinals are Limit Cardinals

Informal description

If a cardinal number $c$ is a strong limit cardinal, then it is also a (weak) limit cardinal. That is, $c \neq 0$ and for every cardinal $x < c$, the successor of $x$ is also less than $c$.

Cardinal.IsStrongLimit.isSuccPrelimit theorem

{c} (H : IsStrongLimit c) : IsSuccPrelimit c

Full source

protected theorem IsStrongLimit.isSuccPrelimit {c} (H : IsStrongLimit c) : IsSuccPrelimit c :=
  H.isSuccLimit.isSuccPrelimit

Strong Limit Cardinals are Successor Pre-Limits

Informal description

If a cardinal number $c$ is a strong limit cardinal, then it is a successor pre-limit. That is, $c$ is nonzero and there does not exist any cardinal $x$ such that $x$ is covered by $c$ (i.e., there is no $x$ with $x \lessdot c$).

Cardinal.le_sum theorem

{ι} (f : ι → Cardinal) (i) : f i ≤ sum f

Full source

theorem le_sum {ι} (f : ι → Cardinal) (i) : f i ≤ sum f := by
  rw [← Quotient.out_eq (f i)]
  exact ⟨⟨fun a => ⟨i, a⟩, fun a b h => by injection h⟩⟩

Cardinal Sum Lower Bound: $κ_i \leq \sum_{j \in ι} κ_j$

Informal description

For any family of cardinals $(κ_i)_{i \in ι}$ indexed by a type $ι$, and for any index $i \in ι$, the cardinal $κ_i$ is less than or equal to the sum of the family $\sum_{j \in ι} κ_j$.

Cardinal.iSup_le_sum theorem

{ι} (f : ι → Cardinal) : iSup f ≤ sum f

Full source

theorem iSup_le_sum {ι} (f : ι → Cardinal) : iSup f ≤ sum f :=
  ciSup_le' <| le_sum _

Supremum Bound for Cardinal Sum: $\bigsqcup_i κ_i \leq \sum_i κ_i$

Informal description

For any family of cardinal numbers $(κ_i)_{i \in \iota}$ indexed by a type $\iota$, the supremum of the family is less than or equal to the sum of the family, i.e., $$\bigsqcup_{i \in \iota} κ_i \leq \sum_{i \in \iota} κ_i.$$

Cardinal.sum_add_distrib theorem

{ι} (f g : ι → Cardinal) : sum (f + g) = sum f + sum g

Full source

@[simp]
theorem sum_add_distrib {ι} (f g : ι → Cardinal) : sum (f + g) = sum f + sum g := by
  have := mk_congr (Equiv.sigmaSumDistrib (Quotient.outQuotient.out ∘ f) (Quotient.outQuotient.out ∘ g))
  simp only [comp_apply, mk_sigma, mk_sum, mk_out, lift_id] at this
  exact this

Distributivity of Sum over Addition for Cardinal Numbers: $\sum (f_i + g_i) = \sum f_i + \sum g_i$

Informal description

For any family of cardinal numbers $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ indexed by a type $\iota$, the sum of the pointwise addition $f_i + g_i$ equals the sum of the individual sums, i.e., $$\sum_{i \in \iota} (f_i + g_i) = \left(\sum_{i \in \iota} f_i\right) + \left(\sum_{i \in \iota} g_i\right).$$

Cardinal.sum_add_distrib' theorem

{ι} (f g : ι → Cardinal) : (Cardinal.sum fun i => f i + g i) = sum f + sum g

Full source

@[simp]
theorem sum_add_distrib' {ι} (f g : ι → Cardinal) :
    (Cardinal.sum fun i => f i + g i) = sum f + sum g :=
  sum_add_distrib f g

Distributivity of Cardinal Sum over Pointwise Addition

Informal description

For any family of cardinal numbers $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ indexed by a type $\iota$, the sum of the pointwise sums $f_i + g_i$ equals the sum of the individual sums, i.e., $$\sum_{i \in \iota} (f_i + g_i) = \left(\sum_{i \in \iota} f_i\right) + \left(\sum_{i \in \iota} g_i\right).$$

Cardinal.sum_le_sum theorem

{ι} (f g : ι → Cardinal) (H : ∀ i, f i ≤ g i) : sum f ≤ sum g

Full source

theorem sum_le_sum {ι} (f g : ι → Cardinal) (H : ∀ i, f i ≤ g i) : sum f ≤ sum g :=
  ⟨(Embedding.refl _).sigmaMap fun i =>
      Classical.choice <| by have := H i; rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this⟩

Monotonicity of Cardinal Sums: $\sum f_i \leq \sum g_i$ when $f_i \leq g_i$ for all $i$

Informal description

For any family of cardinal numbers $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ indexed by a type $\iota$, if $f_i \leq g_i$ for every $i \in \iota$, then the sum of the family $f$ is less than or equal to the sum of the family $g$, i.e., $$\sum_{i \in \iota} f_i \leq \sum_{i \in \iota} g_i.$$

Cardinal.mk_le_mk_mul_of_mk_preimage_le theorem

{c : Cardinal} (f : α → β) (hf : ∀ b : β, #(f ⁻¹' { b }) ≤ c) : #α ≤ #β * c

Full source

theorem mk_le_mk_mul_of_mk_preimage_le {c : Cardinal} (f : α → β) (hf : ∀ b : β, #(f ⁻¹' {b}) ≤ c) :
    #α ≤ #β * c := by
  simpa only [← mk_congr (@Equiv.sigmaFiberEquiv α β f), mk_sigma, ← sum_const'] using
    sum_le_sum _ _ hf

Cardinality Bound via Preimages: $\#\alpha \leq \#\beta \cdot c$ when fibers have cardinality $\leq c$

Informal description

For any function $f : \alpha \to \beta$ and any cardinal number $c$, if for every $b \in \beta$ the cardinality of the preimage $f^{-1}(\{b\})$ is at most $c$, then the cardinality of $\alpha$ is at most the product of the cardinality of $\beta$ and $c$, i.e., $$ \#\alpha \leq \#\beta \cdot c. $$

Cardinal.lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le theorem

 {α : Type u} {β : Type v} {c : Cardinal} (f : α → β) (hf : ∀ b : β, lift.{v} #(f ⁻¹' { b }) ≤ c) :
  lift.{v} #α ≤ lift.{u} #β * c

Full source

theorem lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le {α : Type u} {β : Type v} {c : Cardinal}
    (f : α → β) (hf : ∀ b : β, lift.{v} #(f ⁻¹' {b}) ≤ c) : lift.{v} #α ≤ lift.{u} #β * c :=
  (mk_le_mk_mul_of_mk_preimage_le fun x : ULift.{v} α => ULift.up.{u} (f x.1)) <|
    ULift.forall.2 fun b =>
      (mk_congr <|
            (Equiv.ulift.image _).trans
              (Equiv.trans
                (by
                  rw [Equiv.image_eq_preimage]
                  /- Porting note: Need to insert the following `have` b/c bad fun coercion
                   behaviour for Equivs -/
                  have : DFunLike.coe (Equiv.symm (Equiv.ulift (α := α))) = ULift.up (α := α) := rfl
                  rw [this]
                  simp only [preimage, mem_singleton_iff, ULift.up_inj, mem_setOf_eq, coe_setOf]
                  exact Equiv.refl _)
                Equiv.ulift.symm)).trans_le
        (hf b)

Lifted Cardinality Bound via Preimages: $\#\alpha \leq \#\beta \cdot c$ when fibers have lifted cardinality $\leq c$

Informal description

Let $\alpha$ and $\beta$ be types in universes $u$ and $v$ respectively, and let $c$ be a cardinal number. Given a function $f \colon \alpha \to \beta$ such that for every $b \in \beta$, the cardinality of the preimage $f^{-1}(\{b\})$ (lifted to universe $\max u v$) is at most $c$, then the cardinality of $\alpha$ (lifted to universe $\max u v$) is at most the product of the cardinality of $\beta$ (lifted to universe $\max u v$) and $c$, i.e., $$ \#\alpha \leq \#\beta \cdot c. $$

nonempty_embedding_to_cardinal theorem

: Nonempty (α ↪ Cardinal.{u})

Full source

theorem nonempty_embedding_to_cardinal : Nonempty (α ↪ Cardinal.{u}) :=
  (Embedding.total _ _).resolve_left fun ⟨⟨f, hf⟩⟩ =>
    let g : α → CardinalCardinal.{u} := invFun f
    let ⟨x, (hx : g x = 2 ^ sum g)⟩ := invFun_surjective hf (2 ^ sum g)
    have : g x ≤ sum g := le_sum.{u, u} g x
    not_le_of_gt (by rw [hx]; exact cantor _) this

Existence of an Embedding from Any Type to Cardinal Numbers

Informal description

For any type $\alpha$, there exists an injective function from $\alpha$ to the type of cardinal numbers in the same universe as $\alpha$.

embeddingToCardinal definition

: α ↪ Cardinal.{u}

Full source

/-- An embedding of any type to the set of cardinals in its universe. -/
def embeddingToCardinal : α ↪ Cardinal.{u} :=
  Classical.choice nonempty_embedding_to_cardinal

Embedding from a type to cardinal numbers

Informal description

The function `embeddingToCardinal` is an injective embedding from any type $\alpha$ to the set of cardinal numbers in the same universe as $\alpha$. More precisely, it maps each element of $\alpha$ to its corresponding cardinal number in `Cardinal.{u}`, ensuring that distinct elements of $\alpha$ are mapped to distinct cardinals.

WellOrderingRel definition

: α → α → Prop

Full source

/-- Any type can be endowed with a well order, obtained by pulling back the well order over
cardinals by some embedding. -/
def WellOrderingRel : α → α → Prop :=
  embeddingToCardinalembeddingToCardinal ⁻¹'o (· < ·)

Well-ordering relation via cardinal embedding

Informal description

The relation `WellOrderingRel` on a type $\alpha$ is defined as the preimage of the strict order relation on cardinal numbers under the embedding `embeddingToCardinal`. That is, for any $x, y \in \alpha$, we have $x \leq y$ if and only if the cardinality of $x$ is less than or equal to the cardinality of $y$ in the image of the embedding.

WellOrderingRel.isWellOrder instance

: IsWellOrder α WellOrderingRel

Full source

instance WellOrderingRel.isWellOrder : IsWellOrder α WellOrderingRel :=
  (RelEmbedding.preimage _ _).isWellOrder

Well-Ordering Property of the Cardinal Embedding Relation

Informal description

The relation `WellOrderingRel` on any type $\alpha$ is a well-order. That is, it satisfies the following properties: 1. **Trichotomy**: For any two elements $x, y \in \alpha$, exactly one of the following holds: $x < y$, $x = y$, or $y < x$ under `WellOrderingRel`. 2. **Transitivity**: For any three elements $x, y, z \in \alpha$, if $x < y$ and $y < z$ hold, then $x < z$ also holds. 3. **Well-foundedness**: Every non-empty subset of $\alpha$ has a minimal element with respect to `WellOrderingRel`.

IsWellOrder.subtype_nonempty instance

: Nonempty { r // IsWellOrder α r }

Full source

instance IsWellOrder.subtype_nonempty : Nonempty { r // IsWellOrder α r } :=
  ⟨⟨WellOrderingRel, inferInstance⟩⟩

Existence of Well-Ordering on Any Type

Informal description

For any type $\alpha$, there exists a well-order relation on $\alpha$.

exists_wellOrder theorem

: ∃ (_ : LinearOrder α), WellFoundedLT α

Full source

/-- The **well-ordering theorem** (or **Zermelo's theorem**): every type has a well-order -/
theorem exists_wellOrder : ∃ (_ : LinearOrder α), WellFoundedLT α := by
  classical
  exact ⟨linearOrderOfSTO WellOrderingRel, WellOrderingRel.isWellOrder.toIsWellFounded⟩

Well-ordering theorem: Every type admits a well-order

Informal description

For any type $\alpha$, there exists a linear order relation on $\alpha$ that is well-founded, meaning every non-empty subset of $\alpha$ has a minimal element with respect to this order.

Cardinal.exists_eq_of_iSup_eq_of_not_isSuccPrelimit theorem

 {ι : Type u} (f : ι → Cardinal.{v}) (ω : Cardinal.{v}) (hω : ¬IsSuccPrelimit ω) (h : ⨆ i : ι, f i = ω) : ∃ i, f i = ω

Full source

lemma exists_eq_of_iSup_eq_of_not_isSuccPrelimit
    {ι : Type u} (f : ι → CardinalCardinal.{v}) (ω : CardinalCardinal.{v})
    (hω : ¬ IsSuccPrelimit ω)
    (h : ⨆ i : ι, f i = ω) : ∃ i, f i = ω := by
  subst h
  suffices BddAbove (range f) from (isLUB_csSup' this).mem_of_not_isSuccPrelimit hω
  contrapose! hω with hf
  rw [iSup, csSup_of_not_bddAbove hf, csSup_empty]
  exact isSuccPrelimit_bot

Supremum Attainment for Non-Successor-Prelimit Cardinals: $\bigsqcup_i f(i) = \omega \implies \exists i, f(i) = \omega$

Informal description

Let $\{f(i)\}_{i \in \iota}$ be a family of cardinal numbers indexed by a type $\iota$, and let $\omega$ be a cardinal number that is not a successor pre-limit (i.e., there exists some cardinal $\kappa$ such that $\kappa \lessdot \omega$). If the supremum of the family equals $\omega$ (i.e., $\bigsqcup_{i \in \iota} f(i) = \omega$), then there exists an index $i \in \iota$ such that $f(i) = \omega$.

Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit theorem

 {ι : Type u} [hι : Nonempty ι] (f : ι → Cardinal.{v}) (hf : BddAbove (range f)) {c : Cardinal.{v}}
  (hc : ¬IsSuccLimit c) (h : ⨆ i, f i = c) : ∃ i, f i = c

Full source

lemma exists_eq_of_iSup_eq_of_not_isSuccLimit
    {ι : Type u} [hι : Nonempty ι] (f : ι → CardinalCardinal.{v}) (hf : BddAbove (range f))
    {c : CardinalCardinal.{v}} (hc : ¬ IsSuccLimit c)
    (h : ⨆ i, f i = c) : ∃ i, f i = c := by
  rw [Cardinal.isSuccLimit_iff] at hc
  refine (not_and_or.mp hc).elim (fun e ↦ ⟨hι.some, ?_⟩)
    (Cardinal.exists_eq_of_iSup_eq_of_not_isSuccPrelimit.{u, v} f c · h)
  cases not_not.mp e
  rw [← le_zero_iff] at h ⊢
  exact (le_ciSup hf _).trans h

Supremum Attainment for Non-Successor-Limit Cardinals: $\bigsqcup_i f(i) = c \implies \exists i, f(i) = c$ when $c$ is not a successor limit

Informal description

Let $\{f(i)\}_{i \in \iota}$ be a family of cardinal numbers indexed by a nonempty type $\iota$, with the range of $f$ bounded above. If $c$ is a cardinal number that is not a successor limit (i.e., either $c = 0$ or there exists some cardinal $\kappa$ such that $\kappa < c$ and $\text{succ}(\kappa) \geq c$), and the supremum of the family equals $c$ (i.e., $\bigsqcup_{i \in \iota} f(i) = c$), then there exists an index $i \in \iota$ such that $f(i) = c$.

Cardinal.sum_lt_prod theorem

{ι} (f g : ι → Cardinal) (H : ∀ i, f i < g i) : sum f < prod g

Full source

/-- **König's theorem** -/
theorem sum_lt_prod {ι} (f g : ι → Cardinal) (H : ∀ i, f i < g i) : sum f < prod g :=
  lt_of_not_ge fun ⟨F⟩ => by
    have : Inhabited (∀ i : ι, (g i).out) := by
      refine ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 ?_⟩
      rw [mk_out]
      exact (H i).ne_bot
    let G := invFun F
    have sG : Surjective G := invFun_surjective F.2
    choose C hc using
      show ∀ i, ∃ b, ∀ a, G ⟨i, a⟩ i ≠ b by
        intro i
        simp only [not_exists.symm, not_forall.symm]
        refine fun h => (H i).not_le ?_
        rw [← mk_out (f i), ← mk_out (g i)]
        exact ⟨Embedding.ofSurjective _ h⟩
    let ⟨⟨i, a⟩, h⟩ := sG C
    exact hc i a (congr_fun h _)

König's Theorem: $\sum_{i} f(i) < \prod_{i} g(i)$ when $f(i) < g(i)$ for all $i$

Informal description

For any family of cardinals $\{f(i)\}_{i \in \iota}$ and $\{g(i)\}_{i \in \iota}$ indexed by a type $\iota$, if $f(i) < g(i)$ for every $i \in \iota$, then the sum of the cardinals $\sum_{i \in \iota} f(i)$ is strictly less than the product of the cardinals $\prod_{i \in \iota} g(i)$.

Cardinal.prod_le_prod theorem

{ι} (f g : ι → Cardinal) (H : ∀ i, f i ≤ g i) : prod f ≤ prod g

Full source

theorem prod_le_prod {ι} (f g : ι → Cardinal) (H : ∀ i, f i ≤ g i) : prod f ≤ prod g :=
  ⟨Embedding.piCongrRight fun i =>
      Classical.choice <| by have := H i; rwa [← mk_out (f i), ← mk_out (g i)] at this⟩

Monotonicity of Cardinal Product: $\prod_{i} f(i) \leq \prod_{i} g(i)$ when $f(i) \leq g(i)$ for all $i$

Informal description

For any family of cardinal numbers $\{f(i)\}_{i \in \iota}$ and $\{g(i)\}_{i \in \iota}$ indexed by a type $\iota$, if $f(i) \leq g(i)$ for every $i \in \iota$, then the product cardinal $\prod_{i \in \iota} f(i)$ is less than or equal to the product cardinal $\prod_{i \in \iota} g(i)$.

Cardinal.aleph0_pos theorem

: 0 < ℵ₀

Full source

theorem aleph0_pos : 0 < ℵ₀ :=
  pos_iff_ne_zero.2 aleph0_ne_zero

Positivity of Aleph-null: $0 < \aleph_0$

Informal description

The first infinite cardinal $\aleph_0$ is strictly greater than zero, i.e., $0 < \aleph_0$.

Cardinal.aleph0_le_lift theorem

{c : Cardinal.{u}} : ℵ₀ ≤ lift.{v} c ↔ ℵ₀ ≤ c

Full source

@[simp]
theorem aleph0_le_lift {c : CardinalCardinal.{u}} : ℵ₀ℵ₀ ≤ lift.{v} c ↔ ℵ₀ ≤ c := by
  simpa using lift_le (a := ℵ₀)

Lift Invariance of Aleph-null Inequality: $\aleph_0 \leq \text{lift}(c) \leftrightarrow \aleph_0 \leq c$

Informal description

For any cardinal number $c$ in universe `Type u`, the inequality $\aleph_0 \leq \text{lift}_{v}(c)$ holds if and only if $\aleph_0 \leq c$ holds in the original universe.

Cardinal.lift_le_aleph0 theorem

{c : Cardinal.{u}} : lift.{v} c ≤ ℵ₀ ↔ c ≤ ℵ₀

Full source

@[simp]
theorem lift_le_aleph0 {c : CardinalCardinal.{u}} : liftlift.{v} c ≤ ℵ₀ ↔ c ≤ ℵ₀ := by
  simpa using lift_le (b := ℵ₀)

Lift Preserves Aleph-null Inequality: $\text{lift}(c) \leq \aleph_0 \leftrightarrow c \leq \aleph_0$

Informal description

For any cardinal number $c$ in universe `Type u`, the lift of $c$ to universe `Type (max u v)` is less than or equal to $\aleph_0$ if and only if $c \leq \aleph_0$ in the original universe.

Cardinal.aleph0_lt_lift theorem

{c : Cardinal.{u}} : ℵ₀ < lift.{v} c ↔ ℵ₀ < c

Full source

@[simp]
theorem aleph0_lt_lift {c : CardinalCardinal.{u}} : ℵ₀ℵ₀ < lift.{v} c ↔ ℵ₀ < c := by
  simpa using lift_lt (a := ℵ₀)

Lift Invariance of Aleph-null Strict Inequality: $\aleph_0 < \text{lift}(c) \leftrightarrow \aleph_0 < c$

Informal description

For any cardinal number $c$ in universe `Type u`, the lift of $c$ to universe `Type (max u v)$ satisfies $\aleph_0 < \text{lift}(c)$ if and only if $\aleph_0 < c$ in the original universe.

Cardinal.lift_lt_aleph0 theorem

{c : Cardinal.{u}} : lift.{v} c < ℵ₀ ↔ c < ℵ₀

Full source

@[simp]
theorem lift_lt_aleph0 {c : CardinalCardinal.{u}} : liftlift.{v} c < ℵ₀ ↔ c < ℵ₀ := by
  simpa using lift_lt (b := ℵ₀)

Preservation of Strict Inequality with Aleph-null under Cardinal Lift: $\text{lift}_{v,u}(c) < \aleph_0 \leftrightarrow c < \aleph_0$

Informal description

For any cardinal number $c$ in universe `Type u`, the lift of $c$ to universe `Type (max u v)$ is strictly less than $\aleph_0$ if and only if $c$ is strictly less than $\aleph_0$ in the original universe.

Cardinal.aleph0_eq_lift theorem

{c : Cardinal.{u}} : ℵ₀ = lift.{v} c ↔ ℵ₀ = c

Full source

@[simp]
theorem aleph0_eq_lift {c : CardinalCardinal.{u}} : ℵ₀ℵ₀ = lift.{v} c ↔ ℵ₀ = c := by
  simpa using lift_inj (a := ℵ₀)

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

Informal description

For any cardinal number $c$ in universe `Type u`, the lift of $c$ to universe `Type (max u v)$ satisfies $\aleph_0 = \text{lift}(c)$ if and only if $\aleph_0 = c$ in the original universe.

Cardinal.lift_eq_aleph0 theorem

{c : Cardinal.{u}} : lift.{v} c = ℵ₀ ↔ c = ℵ₀

Full source

@[simp]
theorem lift_eq_aleph0 {c : CardinalCardinal.{u}} : liftlift.{v} c = ℵ₀ ↔ c = ℵ₀ := by
  simpa using lift_inj (b := ℵ₀)

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

Informal description

For any cardinal number $c$ in universe `Type u`, the lift of $c$ to universe `Type (max u v)$ is equal to $\aleph_0$ if and only if $c$ is equal to $\aleph_0$ in the original universe.

Cardinal.mk_fin theorem

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

Full source

theorem mk_fin (n : ℕ) : #(Fin n) = n := by simp

Cardinality of Finite Type $\text{Fin}(n)$ Equals $n$

Informal description

For any natural number $n$, the cardinality of the finite type $\text{Fin}(n)$ (the type of natural numbers less than $n$) is equal to $n$, i.e., $\#(\text{Fin}(n)) = n$.

Cardinal.lift_natCast theorem

(n : ℕ) : lift.{u} (n : Cardinal.{v}) = n

Full source

@[simp]
theorem lift_natCast (n : ℕ) : lift.{u} (n : CardinalCardinal.{v}) = n := by induction n <;> simp [*]

Lift Invariance of Natural Number Cardinals: $\text{lift}(n) = n$

Informal description

For any natural number $n$, the lift of the cardinal number $n$ (viewed as a cardinal in universe `Type v`) to universe `Type (max v u)` is equal to $n$ itself.

Cardinal.lift_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : lift.{u} (ofNat(n) : Cardinal.{v}) = OfNat.ofNat n

Full source

@[simp]
theorem lift_ofNat (n : ℕ) [n.AtLeastTwo] :
    lift.{u} (ofNat(n) : CardinalCardinal.{v}) = OfNat.ofNat n :=
  lift_natCast n

Lift Invariance of Cardinal Numbers $\geq 2$: $\text{lift}(n) = n$ for $n \geq 2$

Informal description

For any natural number $n \geq 2$, the lift of the cardinal number $n$ (viewed as a cardinal in universe `Type v`) to universe `Type (max v u)` is equal to $n$ itself, i.e., $\text{lift}(n) = n$.

Cardinal.lift_eq_nat_iff theorem

{a : Cardinal.{u}} {n : ℕ} : lift.{v} a = n ↔ a = n

Full source

@[simp]
theorem lift_eq_nat_iff {a : CardinalCardinal.{u}} {n : ℕ} : liftlift.{v} a = n ↔ a = n :=
  lift_injective.eq_iff' (lift_natCast n)

Lift Equivalence with Natural Number Cardinals: $\text{lift}(a) = n \leftrightarrow a = n$

Informal description

For any cardinal number $a$ in universe `Type u` and any natural number $n$, the lift of $a$ to universe `Type (max u v)` equals $n$ if and only if $a$ equals $n$.

Cardinal.lift_eq_ofNat_iff theorem

{a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : lift.{v} a = ofNat(n) ↔ a = OfNat.ofNat n

Full source

@[simp]
theorem lift_eq_ofNat_iff {a : CardinalCardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
    liftlift.{v} a = ofNat(n) ↔ a = OfNat.ofNat n :=
  lift_eq_nat_iff

Lift Equivalence with Natural Number Cardinals ≥ 2: $\text{lift}(a) = n \leftrightarrow a = n$ for $n \geq 2$

Informal description

For any cardinal number $a$ in universe `Type u` and any natural number $n \geq 2$, the lift of $a$ to universe `Type (max u v)` equals the cardinal $n$ if and only if $a$ equals $n$.

Cardinal.nat_eq_lift_iff theorem

{n : ℕ} {a : Cardinal.{u}} : (n : Cardinal) = lift.{v} a ↔ (n : Cardinal) = a

Full source

@[simp]
theorem nat_eq_lift_iff {n : ℕ} {a : CardinalCardinal.{u}} :
    (n : Cardinal) = lift.{v} a ↔ (n : Cardinal) = a := by
  rw [← lift_natCast.{v,u} n, lift_inj]

Natural Number Cardinal Equality with Lift: $n = \text{lift}(a) \leftrightarrow n = a$

Informal description

For any natural number $n$ and any cardinal number $a$ in universe `Type u`, the equality $n = \text{lift}_{v}(a)$ holds if and only if $n = a$ in the original universe.

Cardinal.zero_eq_lift_iff theorem

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

Full source

@[simp]
theorem zero_eq_lift_iff {a : CardinalCardinal.{u}} :
    (0 : Cardinal) = lift.{v} a ↔ 0 = a := by
  simpa using nat_eq_lift_iff (n := 0)

Zero Cardinal Equality with Lift: $0 = \text{lift}(a) \leftrightarrow 0 = a$

Informal description

For any cardinal number $a$ in universe `Type u`, the equality $0 = \text{lift}_{v}(a)$ holds if and only if $0 = a$ in the original universe.

Cardinal.one_eq_lift_iff theorem

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

Full source

@[simp]
theorem one_eq_lift_iff {a : CardinalCardinal.{u}} :
    (1 : Cardinal) = lift.{v} a ↔ 1 = a := by
  simpa using nat_eq_lift_iff (n := 1)

One Cardinal Equality with Lift: $1 = \text{lift}(a) \leftrightarrow 1 = a$

Informal description

For any cardinal number $a$ in universe `Type u`, the equality $1 = \text{lift}_{v}(a)$ holds if and only if $1 = a$ in the original universe.

Cardinal.ofNat_eq_lift_iff theorem

{a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : Cardinal) = lift.{v} a ↔ (OfNat.ofNat n : Cardinal) = a

Full source

@[simp]
theorem ofNat_eq_lift_iff {a : CardinalCardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
    (ofNat(n) : Cardinal) = lift.{v} a ↔ (OfNat.ofNat n : Cardinal) = a :=
  nat_eq_lift_iff

Natural Number Cardinal Equality with Lift for $n \geq 2$: $n = \text{lift}(a) \leftrightarrow n = a$

Informal description

For any cardinal number $a$ in universe `Type u` and any natural number $n \geq 2$, the equality $n = \text{lift}_{v}(a)$ holds if and only if $n = a$ in the original universe.

Cardinal.lift_le_nat_iff theorem

{a : Cardinal.{u}} {n : ℕ} : lift.{v} a ≤ n ↔ a ≤ n

Full source

@[simp]
theorem lift_le_nat_iff {a : CardinalCardinal.{u}} {n : ℕ} : liftlift.{v} a ≤ n ↔ a ≤ n := by
  rw [← lift_natCast.{v,u}, lift_le]

Lift Preserves Order with Natural Numbers: $\text{lift}(a) \leq n \leftrightarrow a \leq n$

Informal description

For any cardinal number $a$ in universe `Type u` and any natural number $n$, the lift of $a$ to universe `Type (max u v)` is less than or equal to $n$ if and only if $a \leq n$ in the original universe.

Cardinal.lift_le_one_iff theorem

{a : Cardinal.{u}} : lift.{v} a ≤ 1 ↔ a ≤ 1

Full source

@[simp]
theorem lift_le_one_iff {a : CardinalCardinal.{u}} :
    liftlift.{v} a ≤ 1 ↔ a ≤ 1 := by
  simpa using lift_le_nat_iff (n := 1)

Lift Preserves Order with One: $\text{lift}(a) \leq 1 \leftrightarrow a \leq 1$

Informal description

For any cardinal number $a$ in universe `Type u`, the lift of $a$ to universe `Type (max u v)` is less than or equal to $1$ if and only if $a \leq 1$ in the original universe.

Cardinal.lift_le_ofNat_iff theorem

{a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : lift.{v} a ≤ ofNat(n) ↔ a ≤ OfNat.ofNat n

Full source

@[simp]
theorem lift_le_ofNat_iff {a : CardinalCardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
    liftlift.{v} a ≤ ofNat(n) ↔ a ≤ OfNat.ofNat n :=
  lift_le_nat_iff

Lift Preserves Order with Numerals ≥ 2: $\text{lift}(a) \leq n \leftrightarrow a \leq n$ for $n \geq 2$

Informal description

For any cardinal number $a$ in universe `Type u` and any natural number $n \geq 2$, the lift of $a$ to universe `Type (max u v)` is less than or equal to $n$ if and only if $a \leq n$ in the original universe.

Cardinal.nat_le_lift_iff theorem

{n : ℕ} {a : Cardinal.{u}} : n ≤ lift.{v} a ↔ n ≤ a

Full source

@[simp]
theorem nat_le_lift_iff {n : ℕ} {a : CardinalCardinal.{u}} : n ≤ lift.{v} a ↔ n ≤ a := by
  rw [← lift_natCast.{v,u}, lift_le]

Natural Number Inequality Preserved Under Cardinal Lift: $n \leq \text{lift}(a) \leftrightarrow n \leq a$

Informal description

For any natural number $n$ and any cardinal number $a$ in universe `Type u`, the inequality $n \leq \text{lift}(a)$ holds if and only if $n \leq a$ holds in the original universe, where $\text{lift}(a)$ denotes the lift of $a$ to universe `Type (max u v)`.

Cardinal.one_le_lift_iff theorem

{a : Cardinal.{u}} : (1 : Cardinal) ≤ lift.{v} a ↔ 1 ≤ a

Full source

@[simp]
theorem one_le_lift_iff {a : CardinalCardinal.{u}} :
    (1 : Cardinal) ≤ lift.{v} a ↔ 1 ≤ a := by
  simpa using nat_le_lift_iff (n := 1)

Preservation of One Inequality under Cardinal Lift: $1 \leq \text{lift}(a) \leftrightarrow 1 \leq a$

Informal description

For any cardinal number $a$ in universe `Type u`, the lift of $a$ to universe `Type (max u v)$ satisfies $1 \leq \text{lift}(a)$ if and only if $1 \leq a$ holds in the original universe.

Cardinal.ofNat_le_lift_iff theorem

{a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : Cardinal) ≤ lift.{v} a ↔ (OfNat.ofNat n : Cardinal) ≤ a

Full source

@[simp]
theorem ofNat_le_lift_iff {a : CardinalCardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
    (ofNat(n) : Cardinal) ≤ lift.{v} a ↔ (OfNat.ofNat n : Cardinal) ≤ a :=
  nat_le_lift_iff

Preservation of Natural Number Inequality under Cardinal Lift: $n \leq \text{lift}(a) \leftrightarrow n \leq a$

Informal description

For any natural number $n \geq 2$ and any cardinal number $a$ in universe `Type u`, the inequality $n \leq \text{lift}(a)$ holds if and only if $n \leq a$ holds in the original universe, where $\text{lift}(a)$ denotes the lift of $a$ to universe `Type (max u v)$.

Cardinal.lift_lt_nat_iff theorem

{a : Cardinal.{u}} {n : ℕ} : lift.{v} a < n ↔ a < n

Full source

@[simp]
theorem lift_lt_nat_iff {a : CardinalCardinal.{u}} {n : ℕ} : liftlift.{v} a < n ↔ a < n := by
  rw [← lift_natCast.{v,u}, lift_lt]

Preservation of Strict Inequality with Natural Numbers under Cardinal Lift: $\text{lift}(a) < n \leftrightarrow a < n$

Informal description

For any cardinal number $a$ in universe `Type u` and any natural number $n$, the lift of $a$ to universe `Type (max u v)$ is strictly less than $n$ if and only if $a$ is strictly less than $n$ in the original universe.

Cardinal.lift_lt_ofNat_iff theorem

{a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : lift.{v} a < ofNat(n) ↔ a < OfNat.ofNat n

Full source

@[simp]
theorem lift_lt_ofNat_iff {a : CardinalCardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
    liftlift.{v} a < ofNat(n) ↔ a < OfNat.ofNat n :=
  lift_lt_nat_iff

Preservation of Strict Inequality with Numerals ≥ 2 under Cardinal Lift: $\text{lift}(a) < n \leftrightarrow a < n$ for $n \geq 2$

Informal description

For any cardinal number $a$ in universe `Type u` and any natural number $n \geq 2$, the lift of $a$ to universe `Type (max u v)$ is strictly less than $n$ if and only if $a$ is strictly less than $n$ in the original universe.

Cardinal.nat_lt_lift_iff theorem

{n : ℕ} {a : Cardinal.{u}} : n < lift.{v} a ↔ n < a

Full source

@[simp]
theorem nat_lt_lift_iff {n : ℕ} {a : CardinalCardinal.{u}} : n < lift.{v} a ↔ n < a := by
  rw [← lift_natCast.{v,u}, lift_lt]

Preservation of Natural Number Order under Cardinal Lift: $n < \text{lift}_{v}(a) \leftrightarrow n < a$

Informal description

For any natural number $n$ and cardinal number $a$ in universe `Type u`, the inequality $n < \text{lift}_{v}(a)$ holds if and only if $n < a$ holds in the original universe.

Cardinal.zero_lt_lift_iff theorem

{a : Cardinal.{u}} : (0 : Cardinal) < lift.{v} a ↔ 0 < a

Full source

@[simp]
theorem zero_lt_lift_iff {a : CardinalCardinal.{u}} :
    (0 : Cardinal) < lift.{v} a ↔ 0 < a := by
  simpa using nat_lt_lift_iff (n := 0)

Preservation of Zero Order under Cardinal Lift: $0 < \text{lift}_{v}(a) \leftrightarrow 0 < a$

Informal description

For any cardinal number $a$ in universe `Type u`, the lift of $a$ to a higher universe `Type (max u v)` is greater than zero if and only if $a$ is greater than zero in the original universe. That is, $0 < \text{lift}_{v}(a) \leftrightarrow 0 < a$.

Cardinal.one_lt_lift_iff theorem

{a : Cardinal.{u}} : (1 : Cardinal) < lift.{v} a ↔ 1 < a

Full source

@[simp]
theorem one_lt_lift_iff {a : CardinalCardinal.{u}} :
    (1 : Cardinal) < lift.{v} a ↔ 1 < a := by
  simpa using nat_lt_lift_iff (n := 1)

Preservation of One Inequality under Cardinal Lift: $1 < \text{lift}_{v}(a) \leftrightarrow 1 < a$

Informal description

For any cardinal number $a$ in universe `Type u`, the inequality $1 < \text{lift}_{v}(a)$ holds if and only if $1 < a$ holds in the original universe.

Cardinal.ofNat_lt_lift_iff theorem

{a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : Cardinal) < lift.{v} a ↔ (OfNat.ofNat n : Cardinal) < a

Full source

@[simp]
theorem ofNat_lt_lift_iff {a : CardinalCardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
    (ofNat(n) : Cardinal) < lift.{v} a ↔ (OfNat.ofNat n : Cardinal) < a :=
  nat_lt_lift_iff

Preservation of Numeric Order under Cardinal Lift: $n < \text{lift}_{v}(a) \leftrightarrow n < a$

Informal description

For any natural number $n \geq 2$ and any cardinal number $a$ in universe `Type u`, the inequality $n < \text{lift}_{v}(a)$ holds if and only if $n < a$ holds in the original universe.

Cardinal.mk_coe_finset theorem

{α : Type u} {s : Finset α} : #s = ↑(Finset.card s)

Full source

theorem mk_coe_finset {α : Type u} {s : Finset α} : #s = ↑(Finset.card s) := by simp

Cardinality of Finite Subset Equals Its Size

Informal description

For any type $\alpha$ and any finite subset $s$ of $\alpha$ (represented as a `Finset`), the cardinality of $s$ is equal to the natural number representing the size of $s$ (as given by `Finset.card`), when both are viewed as cardinal numbers. That is, $\#s = \text{Finset.card}(s)$.

Cardinal.card_le_of_finset theorem

{α} (s : Finset α) : (s.card : Cardinal) ≤ #α

Full source

theorem card_le_of_finset {α} (s : Finset α) : (s.card : Cardinal) ≤ #α :=
  @mk_coe_finset _ s ▸ mk_set_le _

Finite Subset Cardinality Bound: $|s| \leq \#\alpha$

Informal description

For any finite subset $s$ of a type $\alpha$, the cardinality of $s$ (as a natural number) is less than or equal to the cardinality of $\alpha$ (as a cardinal number). In other words, if $s$ is a finite subset of $\alpha$, then $|s| \leq \#\alpha$.

Cardinal.instCharZero instance

: CharZero Cardinal

Full source

instance : CharZero Cardinal := by
  refine ⟨fun a b h ↦ ?_⟩
  rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h

Cardinals Have Characteristic Zero

Informal description

The type of cardinal numbers has characteristic zero, meaning the canonical embedding of the natural numbers into cardinals is injective.

Mathlib.SetTheory.Cardinal.Order

Main definitions

Main instances

Main Statements

Implementation notes

References

Tags