Cardinal Numbers #

We define cardinal numbers as a quotient of types under the equivalence relation of equinumerity.

Main definitions #

Cardinal is the type of cardinal numbers (in a given universe).
Cardinal.mk α or #α is the cardinality of α. The notation # lives in the locale Cardinal.
Addition c₁ + c₂ is defined by Cardinal.add_def α β : #α + #β = #(α ⊕ β).
Multiplication c₁ * c₂ is defined by Cardinal.mul_def : #α * #β = #(α × β).
The order c₁ ≤ c₂ is defined by Cardinal.le_def α β : #α ≤ #β ↔ Nonempty (α ↪ β).
Exponentiation c₁ ^ c₂ is defined by Cardinal.power_def α β : #α ^ #β = #(β → α).
Cardinal.isLimit c means that c is a (weak) limit cardinal: c ≠ 0 ∧ ∀ x < c, succ x < c.
Cardinal.aleph0 or ℵ₀ is the cardinality of ℕ. This definition is universe polymorphic: Cardinal.aleph0.{u} : Cardinal.{u} (contrast with ℕ : Type, which lives in a specific universe). In some cases the universe level has to be given explicitly.
Cardinal.sum is the sum of an indexed family of cardinals, i.e. the cardinality of the corresponding sigma type.
Cardinal.prod is the product of an indexed family of cardinals, i.e. the cardinality of the corresponding pi type.
Cardinal.powerlt a b or a ^< b is defined as the supremum of a ^ c for c < b.

Main instances #

Cardinals form a CanonicallyOrderedCommSemiring with the aforementioned sum and product.
Cardinals form a SuccOrder. Use Order.succ c for the smallest cardinal greater than c.
The less than relation on cardinals forms a well-order.
Cardinals form a ConditionallyCompleteLinearOrderBot. Bounded sets for cardinals in universe u are precisely the sets indexed by some type in universe u, see Cardinal.bddAbove_iff_small. One can use sSup for the cardinal supremum, and sInf for the minimum of a set of cardinals.

Main Statements #

Cantor's theorem: Cardinal.cantor c : c < 2 ^ c.
König's theorem: Cardinal.sum_lt_prod

Implementation notes #

There is a type of cardinal numbers in every universe level: Cardinal.{u} : Type (u + 1) is the quotient of types in Type u. The operation Cardinal.lift lifts cardinal numbers to a higher level.
Cardinal arithmetic specifically for infinite cardinals (like κ * κ = κ) is in the file Mathlib/SetTheory/Cardinal/Ordinal.lean.
There is an instance Pow Cardinal, but this will only fire if Lean already knows that both the base and the exponent live in the same universe. As a workaround, you can add
```
  local infixr:80 " ^' " => @HPow.hPow Cardinal Cardinal Cardinal _
```
to a file. This notation will work even if Lean doesn't know yet that the base and the exponent live in the same universe (but no exponents in other types can be used). (Porting note: This last point might need to be updated.)

References #

https://en.wikipedia.org/wiki/Cardinal_number

Tags #

cardinal number, cardinal arithmetic, cardinal exponentiation, aleph, Cantor's theorem, König's theorem, Konig's theorem

source

instance Cardinal.isEquivalent :

Setoid (Type u)

The equivalence relation on types given by equivalence (bijective correspondence) of types. Quotienting by this equivalence relation gives the cardinal numbers.

Equations

Cardinal.isEquivalent = { r := fun (α β : Type u) => Nonempty (α ≃ β), iseqv := Cardinal.isEquivalent.proof_1 }

source

def Cardinal :

Type (u + 1)

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).

Equations

Cardinal.{u} = Quotient Cardinal.isEquivalent

Instances For

source

def Cardinal.mk :

Type u → Cardinal.{u}

The cardinal number of a type

Equations

Cardinal.mk = Quotient.mk'

Instances For

source

def Cardinal.«term#_» :

Lean.ParserDescr

The cardinal number of a type

Equations

Cardinal.«term#_» = Lean.ParserDescr.node `Cardinal.term#_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

Instances For

source

instance Cardinal.canLiftCardinalType :

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

Equations

Cardinal.canLiftCardinalType = ⋯

source

theorem Cardinal.inductionOn {p : Cardinal.{u_1} → Prop} (c : Cardinal.{u_1}) (h : ∀ (α : Type u_1), p (Cardinal.mk α)) :

p c

source

theorem Cardinal.inductionOn₂ {p : Cardinal.{u_1} → Cardinal.{u_2} → Prop} (c₁ : Cardinal.{u_1}) (c₂ : Cardinal.{u_2}) (h : ∀ (α : Type u_1) (β : Type u_2), p (Cardinal.mk α) (Cardinal.mk β)) :

p c₁ c₂

source

theorem Cardinal.inductionOn₃ {p : Cardinal.{u_1} → Cardinal.{u_2} → Cardinal.{u_3} → Prop} (c₁ : Cardinal.{u_1}) (c₂ : Cardinal.{u_2}) (c₃ : Cardinal.{u_3}) (h : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), p (Cardinal.mk α) (Cardinal.mk β) (Cardinal.mk γ)) :

p c₁ c₂ c₃

source

theorem Cardinal.eq {α : Type u} {β : Type u} :

Cardinal.mk α = Cardinal.mk β ↔ Nonempty (α ≃ β)

source

@[simp]

theorem Cardinal.mk'_def (α : Type u) :

⟦α⟧ = Cardinal.mk α

source

@[simp]

theorem Cardinal.mk_out (c : Cardinal.{u_1}) :

Cardinal.mk (Quotient.out c) = c

source

def Cardinal.outMkEquiv {α : Type v} :

Quotient.out (Cardinal.mk α) ≃ α

The representative of the cardinal of a type is equivalent to the original type.

Equations

Cardinal.outMkEquiv = ⋯.some

Instances For

source

theorem Cardinal.mk_congr {α : Type u} {β : Type u} (e : α ≃ β) :

Cardinal.mk α = Cardinal.mk β

source

theorem Equiv.cardinal_eq {α : Type u} {β : Type u} (e : α ≃ β) :

Cardinal.mk α = Cardinal.mk β

Alias of Cardinal.mk_congr.

source

def Cardinal.map (f : Type u → Type v) (hf : (α β : Type u) → α ≃ β → f α ≃ f β) :

Cardinal.{u} → Cardinal.{v}

Lift a function between Type*s to a function between Cardinals.

Equations

Cardinal.map f hf = Quotient.map f ⋯

Instances For

source

@[simp]

theorem Cardinal.map_mk (f : Type u → Type v) (hf : (α β : Type u) → α ≃ β → f α ≃ f β) (α : Type u) :

Cardinal.map f hf (Cardinal.mk α) = Cardinal.mk (f α)

source

def Cardinal.map₂ (f : Type u → Type v → Type w) (hf : (α β : Type u) → (γ δ : Type v) → α ≃ β → γ ≃ δ → f α γ ≃ f β δ) :

Cardinal.{u} → Cardinal.{v} → Cardinal.{w}

Lift a binary operation Type* → Type* → Type* to a binary operation on Cardinals.

Equations

Cardinal.map₂ f hf = Quotient.map₂ f ⋯

Instances For

source

def Cardinal.lift (c : Cardinal.{v}) :

Cardinal.{max v u}

The universe lift operation on cardinals. You can specify the universes explicitly with lift.{u v} : Cardinal.{v} → Cardinal.{max v u}

Equations

Cardinal.lift.{u, v} c = Cardinal.map ULift.{u, v} (fun (x x_1 : Type v) (e : x ≃ x_1) => Equiv.ulift.trans (e.trans Equiv.ulift.symm)) c

Instances For

source

@[simp]

theorem Cardinal.mk_uLift (α : Type u) :

Cardinal.mk (ULift.{v, u} α) = Cardinal.lift.{v, u} (Cardinal.mk α)

source

@[simp]

theorem Cardinal.lift_umax :

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

lift.{max u v, u} equals lift.{v, u}.

source

@[simp]

theorem Cardinal.lift_umax' :

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

lift.{max v u, u} equals lift.{v, u}.

source

@[simp]

theorem Cardinal.lift_id' (a : Cardinal.{max u v} ) :

Cardinal.lift.{u, max u v} a = a

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

source

@[simp]

theorem Cardinal.lift_id (a : Cardinal.{u}) :

Cardinal.lift.{u, u} a = a

A cardinal lifted to the same universe equals itself.

source

theorem Cardinal.lift_uzero (a : Cardinal.{u}) :

Cardinal.lift.{0, u} a = a

A cardinal lifted to the zero universe equals itself.

source

@[simp]

theorem Cardinal.lift_lift (a : Cardinal.{u_1}) :

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

source

instance Cardinal.instLE :

LE Cardinal.{u}

We define the order on cardinal numbers by #α ≤ #β if and only if there exists an embedding (injective function) from α to β.

Equations

Cardinal.instLE = { le := fun (q₁ q₂ : Cardinal.{u}) => Quotient.liftOn₂ q₁ q₂ (fun (α β : Type u) => Nonempty (α ↪ β)) Cardinal.instLE.proof_1 }

source

instance Cardinal.partialOrder :

PartialOrder Cardinal.{u}

Equations

Cardinal.partialOrder = PartialOrder.mk Cardinal.partialOrder.proof_4

source

instance Cardinal.linearOrder :

LinearOrder Cardinal.{u}

Equations

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

source

theorem Cardinal.le_def (α : Type u) (β : Type u) :

Cardinal.mk α ≤ Cardinal.mk β ↔ Nonempty (α ↪ β)

source

theorem Cardinal.mk_le_of_injective {α : Type u} {β : Type u} {f : α → β} (hf : Function.Injective f) :

Cardinal.mk α ≤ Cardinal.mk β

source

theorem Function.Embedding.cardinal_le {α : Type u} {β : Type u} (f : α ↪ β) :

Cardinal.mk α ≤ Cardinal.mk β

source

theorem Cardinal.mk_le_of_surjective {α : Type u} {β : Type u} {f : α → β} (hf : Function.Surjective f) :

Cardinal.mk β ≤ Cardinal.mk α

source

theorem Cardinal.le_mk_iff_exists_set {c : Cardinal.{u}} {α : Type u} :

c ≤ Cardinal.mk α ↔ ∃ (p : Set α), Cardinal.mk ↑p = c

source

theorem Cardinal.mk_subtype_le {α : Type u} (p : α → Prop) :

Cardinal.mk (Subtype p) ≤ Cardinal.mk α

source

theorem Cardinal.mk_set_le {α : Type u} (s : Set α) :

Cardinal.mk ↑s ≤ Cardinal.mk α

source

@[simp]

theorem Cardinal.mk_preimage_down {α : Type u} {s : Set α} :

Cardinal.mk ↑(ULift.down ⁻¹' s) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)

source

theorem Cardinal.out_embedding {c : Cardinal.{u_1}} {c' : Cardinal.{u_1}} :

c ≤ c' ↔ Nonempty (Quotient.out c ↪ Quotient.out c')

source

theorem Cardinal.lift_mk_le {α : Type v} {β : Type w} :

Cardinal.lift.{max u w, v} (Cardinal.mk α) ≤ Cardinal.lift.{max u v, w} (Cardinal.mk β) ↔ Nonempty (α ↪ β)

source

theorem Cardinal.lift_mk_le' {α : Type u} {β : Type v} :

Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β) ↔ Nonempty (α ↪ β)

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.

source

theorem Cardinal.lift_mk_eq {α : Type u} {β : Type v} :

Cardinal.lift.{max v w, u} (Cardinal.mk α) = Cardinal.lift.{max u w, v} (Cardinal.mk β) ↔ Nonempty (α ≃ β)

source

theorem Cardinal.lift_mk_eq' {α : Type u} {β : Type v} :

Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β) ↔ Nonempty (α ≃ β)

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.

source

@[simp]

theorem Cardinal.lift_le {a : Cardinal.{v}} {b : Cardinal.{v}} :

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

source

@[simp]

theorem Cardinal.liftOrderEmbedding_apply :

⇑Cardinal.liftOrderEmbedding = Cardinal.lift.{u, v}

source

def Cardinal.liftOrderEmbedding :

Cardinal.{v} ↪o Cardinal.{max v u}

Cardinal.lift as an OrderEmbedding.

Equations

Cardinal.liftOrderEmbedding = OrderEmbedding.ofMapLEIff Cardinal.lift.{u, v} ⋯

Instances For

source

theorem Cardinal.lift_injective :

Function.Injective Cardinal.lift.{u, v}

source

@[simp]

theorem Cardinal.lift_inj {a : Cardinal.{u}} {b : Cardinal.{u}} :

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

source

@[simp]

theorem Cardinal.lift_lt {a : Cardinal.{u}} {b : Cardinal.{u}} :

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

source

theorem Cardinal.lift_strictMono :

StrictMono Cardinal.lift.{u_2, u_1}

source

theorem Cardinal.lift_monotone :

Monotone Cardinal.lift.{u_2, u_1}

source

instance Cardinal.instZero :

Zero Cardinal.{u}

Equations

Cardinal.instZero = { zero := Cardinal.lift.{u, 0} (Cardinal.mk (Fin 0)) }

source

instance Cardinal.instInhabited :

Inhabited Cardinal.{u}

Equations

Cardinal.instInhabited = { default := 0 }

source

@[simp]

theorem Cardinal.mk_eq_zero (α : Type u) [IsEmpty α] :

Cardinal.mk α = 0

source

@[simp]

theorem Cardinal.lift_zero :

Cardinal.lift.{u_2, u_1} 0 = 0

source

@[simp]

theorem Cardinal.lift_eq_zero {a : Cardinal.{v}} :

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

source

theorem Cardinal.mk_eq_zero_iff {α : Type u} :

Cardinal.mk α = 0 ↔ IsEmpty α

source

theorem Cardinal.mk_ne_zero_iff {α : Type u} :

Cardinal.mk α ≠ 0 ↔ Nonempty α

source

@[simp]

theorem Cardinal.mk_ne_zero (α : Type u) [Nonempty α] :

Cardinal.mk α ≠ 0

source

instance Cardinal.instOne :

One Cardinal.{u}

Equations

Cardinal.instOne = { one := Cardinal.lift.{u, 0} (Cardinal.mk (Fin 1)) }

source

instance Cardinal.instNontrivial :

Nontrivial Cardinal.{u}

Equations

Cardinal.instNontrivial = ⋯

source

theorem Cardinal.mk_eq_one (α : Type u) [Unique α] :

Cardinal.mk α = 1

source

theorem Cardinal.le_one_iff_subsingleton {α : Type u} :

Cardinal.mk α ≤ 1 ↔ Subsingleton α

source

@[simp]

theorem Cardinal.mk_le_one_iff_set_subsingleton {α : Type u} {s : Set α} :

Cardinal.mk ↑s ≤ 1 ↔ s.Subsingleton

source

theorem Set.Subsingleton.cardinal_mk_le_one {α : Type u} {s : Set α} :

s.Subsingleton → Cardinal.mk ↑s ≤ 1

Alias of the reverse direction of Cardinal.mk_le_one_iff_set_subsingleton.

source

instance Cardinal.instAdd :

Add Cardinal.{u}

Equations

Cardinal.instAdd = { add := Cardinal.map₂ Sum fun (x x_1 x_2 x_3 : Type u) => Equiv.sumCongr }

source

theorem Cardinal.add_def (α : Type u) (β : Type u) :

Cardinal.mk α + Cardinal.mk β = Cardinal.mk (α ⊕ β)

source

instance Cardinal.instNatCast :

NatCast Cardinal.{u}

Equations

Cardinal.instNatCast = { natCast := fun (n : ℕ) => Cardinal.lift.{u, 0} (Cardinal.mk (Fin n)) }

source

@[simp]

theorem Cardinal.mk_sum (α : Type u) (β : Type v) :

Cardinal.mk (α ⊕ β) = Cardinal.lift.{v, u} (Cardinal.mk α) + Cardinal.lift.{u, v} (Cardinal.mk β)

source

@[simp]

theorem Cardinal.mk_option {α : Type u} :

Cardinal.mk (Option α) = Cardinal.mk α + 1

source

@[simp]

theorem Cardinal.mk_psum (α : Type u) (β : Type v) :

Cardinal.mk (α ⊕' β) = Cardinal.lift.{v, u} (Cardinal.mk α) + Cardinal.lift.{u, v} (Cardinal.mk β)

source

@[simp]

theorem Cardinal.mk_fintype (α : Type u) [h : Fintype α] :

Cardinal.mk α = ↑(Fintype.card α)

source

theorem Cardinal.cast_succ (n : ℕ) :

↑(n + 1) = ↑n + 1

source

instance Cardinal.instMul :

Mul Cardinal.{u}

Equations

Cardinal.instMul = { mul := Cardinal.map₂ Prod fun (x x_1 x_2 x_3 : Type u) => Equiv.prodCongr }

source

theorem Cardinal.mul_def (α : Type u) (β : Type u) :

Cardinal.mk α * Cardinal.mk β = Cardinal.mk (α × β)

source

@[simp]

theorem Cardinal.mk_prod (α : Type u) (β : Type v) :

Cardinal.mk (α × β) = Cardinal.lift.{v, u} (Cardinal.mk α) * Cardinal.lift.{u, v} (Cardinal.mk β)

source

instance Cardinal.instPowCardinal :

Pow Cardinal.{u} Cardinal.{u}

The cardinal exponential. #α ^ #β is the cardinal of β → α.

Equations

Cardinal.instPowCardinal = { pow := Cardinal.map₂ (fun (α β : Type u) => β → α) fun (x x_1 x_2 x_3 : Type u) (e₁ : x ≃ x_1) (e₂ : x_2 ≃ x_3) => e₂.arrowCongr e₁ }

source

theorem Cardinal.power_def (α : Type u) (β : Type u) :

Cardinal.mk α ^ Cardinal.mk β = Cardinal.mk (β → α)

source

theorem Cardinal.mk_arrow (α : Type u) (β : Type v) :

Cardinal.mk (α → β) = Cardinal.lift.{u, v} (Cardinal.mk β) ^ Cardinal.lift.{v, u} (Cardinal.mk α)

source

@[simp]

theorem Cardinal.lift_power (a : Cardinal.{u}) (b : Cardinal.{u}) :

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

source

@[simp]

theorem Cardinal.power_zero {a : Cardinal.{u_1}} :

a ^ 0 = 1

source

@[simp]

theorem Cardinal.power_one {a : Cardinal.{u}} :

a ^ 1 = a

source

theorem Cardinal.power_add {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} :

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

source

instance Cardinal.commSemiring :

CommSemiring Cardinal.{u}

Equations

Cardinal.commSemiring = CommSemiring.mk Cardinal.mul_comm'

source

@[simp]

theorem Cardinal.one_power {a : Cardinal.{u_1}} :

1 ^ a = 1

source

theorem Cardinal.mk_bool :

Cardinal.mk Bool = 2

source

theorem Cardinal.mk_Prop :

Cardinal.mk Prop = 2

source

@[simp]

theorem Cardinal.zero_power {a : Cardinal.{u_1}} :

a ≠ 0 → 0 ^ a = 0

source

theorem Cardinal.power_ne_zero {a : Cardinal.{u_1}} (b : Cardinal.{u_1}) :

a ≠ 0 → a ^ b ≠ 0

source

theorem Cardinal.mul_power {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} :

(a * b) ^ c = a ^ c * b ^ c

source

theorem Cardinal.power_mul {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} :

a ^ (b * c) = (a ^ b) ^ c

source

@[simp]

theorem Cardinal.pow_cast_right (a : Cardinal.{u}) (n : ℕ) :

a ^ ↑n = a ^ n

source

@[simp]

theorem Cardinal.lift_one :

Cardinal.lift.{u_2, u_1} 1 = 1

source

@[simp]

theorem Cardinal.lift_eq_one {a : Cardinal.{v}} :

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

source

@[simp]

theorem Cardinal.lift_add (a : Cardinal.{u}) (b : Cardinal.{u}) :

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

source

@[simp]

theorem Cardinal.lift_mul (a : Cardinal.{u}) (b : Cardinal.{u}) :

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

source

theorem Cardinal.lift_two :

Cardinal.lift.{u, v} 2 = 2

source

@[simp]

theorem Cardinal.mk_set {α : Type u} :

Cardinal.mk (Set α) = 2 ^ Cardinal.mk α

source

@[simp]

theorem Cardinal.mk_powerset {α : Type u} (s : Set α) :

Cardinal.mk ↑(𝒫 s) = 2 ^ Cardinal.mk ↑s

A variant of Cardinal.mk_set expressed in terms of a Set instead of a Type.

source

theorem Cardinal.lift_two_power (a : Cardinal.{u_1}) :

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

source

theorem Cardinal.zero_le (a : Cardinal.{u_1}) :

0 ≤ a

source

instance Cardinal.add_covariantClass :

CovariantClass Cardinal.{u_1} Cardinal.{u_1} (fun (x x_1 : Cardinal.{u_1}) => x + x_1) fun (x x_1 : Cardinal.{u_1}) => x ≤ x_1

Equations

Cardinal.add_covariantClass = ⋯

source

instance Cardinal.add_swap_covariantClass :

CovariantClass Cardinal.{u_1} Cardinal.{u_1} (Function.swap fun (x x_1 : Cardinal.{u_1}) => x + x_1) fun (x x_1 : Cardinal.{u_1}) => x ≤ x_1

Equations

Cardinal.add_swap_covariantClass = ⋯

source

instance Cardinal.canonicallyOrderedCommSemiring :

CanonicallyOrderedCommSemiring Cardinal.{u}

Equations

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

source

instance Cardinal.instCanonicallyLinearOrderedAddCommMonoid :

CanonicallyLinearOrderedAddCommMonoid Cardinal.{u}

Equations

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

source

instance Cardinal.instCanonicallyOrderedAddCommMonoid :

CanonicallyOrderedAddCommMonoid Cardinal.{u}

Equations

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

source

instance Cardinal.instLinearOrderedCommMonoidWithZero :

LinearOrderedCommMonoidWithZero Cardinal.{u}

Equations

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

source

instance Cardinal.instCommMonoidWithZero :

CommMonoidWithZero Cardinal.{u}

Equations

Cardinal.instCommMonoidWithZero = let __src := Cardinal.canonicallyOrderedCommSemiring; CommMonoidWithZero.mk ⋯ ⋯

source

instance Cardinal.instCommMonoid :

CommMonoid Cardinal.{u}

Equations

Cardinal.instCommMonoid = let __src := Cardinal.canonicallyOrderedCommSemiring; CommMonoid.mk ⋯

source

theorem Cardinal.zero_power_le (c : Cardinal.{u}) :

0 ^ c ≤ 1

source

theorem Cardinal.power_le_power_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} :

a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c

source

theorem Cardinal.self_le_power (a : Cardinal.{u_1}) {b : Cardinal.{u_1}} (hb : 1 ≤ b) :

a ≤ a ^ b

source

theorem Cardinal.cantor (a : Cardinal.{u}) :

a < 2 ^ a

Cantor's theorem

source

instance Cardinal.instNoMaxOrder :

NoMaxOrder Cardinal.{u}

Equations

Cardinal.instNoMaxOrder = ⋯

source

instance Cardinal.instDistribLattice :

DistribLattice Cardinal.{u}

Equations

Cardinal.instDistribLattice = inferInstance

source

theorem Cardinal.one_lt_iff_nontrivial {α : Type u} :

1 < Cardinal.mk α ↔ Nontrivial α

source

theorem Cardinal.power_le_max_power_one {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (h : b ≤ c) :

a ^ b ≤ max (a ^ c) 1

source

theorem Cardinal.power_le_power_right {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} :

a ≤ b → a ^ c ≤ b ^ c

source

theorem Cardinal.power_pos {a : Cardinal.{u_1}} (b : Cardinal.{u_1}) (ha : 0 < a) :

0 < a ^ b

source

theorem Cardinal.lt_wf :

WellFounded fun (x x_1 : Cardinal.{u}) => x < x_1

source

instance Cardinal.instWellFoundedRelation :

WellFoundedRelation Cardinal.{u}

Equations

Cardinal.instWellFoundedRelation = { rel := fun (x x_1 : Cardinal.{u}) => x < x_1, wf := Cardinal.lt_wf }

source

instance Cardinal.instWellFoundedLT :

WellFoundedLT Cardinal.{u}

Equations

Cardinal.instWellFoundedLT = ⋯

source

instance Cardinal.wo :

IsWellOrder Cardinal.{u} fun (x x_1 : Cardinal.{u}) => x < x_1

Equations

Cardinal.wo = ⋯

source

instance Cardinal.instConditionallyCompleteLinearOrderBot :

ConditionallyCompleteLinearOrderBot Cardinal.{u_1}

Equations

Cardinal.instConditionallyCompleteLinearOrderBot = IsWellOrder.conditionallyCompleteLinearOrderBot Cardinal.{u_1}

source

@[simp]

theorem Cardinal.sInf_empty :

sInf ∅ = 0

source

theorem Cardinal.sInf_eq_zero_iff {s : Set Cardinal.{u_1}} :

sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0

source

theorem Cardinal.iInf_eq_zero_iff {ι : Sort u_1} {f : ι → Cardinal.{u_2}} :

⨅ (i : ι), f i = 0 ↔ IsEmpty ι ∨ ∃ (i : ι), f i = 0

source

instance Cardinal.instSuccOrder :

SuccOrder Cardinal.{u_1}

Note that the successor of c is not the same as c + 1 except in the case of finite c.

Equations

Cardinal.instSuccOrder = SuccOrder.ofSuccLeIff (fun (c : Cardinal.{u_1}) => sInf {c' : Cardinal.{u_1} | c < c'}) @Cardinal.instSuccOrder.proof_1

source

theorem Cardinal.succ_def (c : Cardinal.{u_1}) :

Order.succ c = sInf {c' : Cardinal.{u_1} | c < c'}

source

theorem Cardinal.succ_pos (c : Cardinal.{u_1}) :

0 < Order.succ c

source

theorem Cardinal.succ_ne_zero (c : Cardinal.{u_1}) :

Order.succ c ≠ 0

source

theorem Cardinal.add_one_le_succ (c : Cardinal.{u}) :

c + 1 ≤ Order.succ c

source

def Cardinal.IsLimit (c : Cardinal.{u_1}) :

Prop

A cardinal is a limit if it is not zero or a successor cardinal. Note that ℵ₀ is a limit cardinal by this definition, but 0 isn't.

Use IsSuccLimit if you want to include the c = 0 case.

Equations

c.IsLimit = (c ≠ 0 ∧ Order.IsSuccLimit c)

Instances For

source

theorem Cardinal.IsLimit.ne_zero {c : Cardinal.{u_1}} (h : c.IsLimit) :

c ≠ 0

source

theorem Cardinal.IsLimit.isSuccLimit {c : Cardinal.{u_1}} (h : c.IsLimit) :

Order.IsSuccLimit c

source

theorem Cardinal.IsLimit.succ_lt {x : Cardinal.{u_1}} {c : Cardinal.{u_1}} (h : c.IsLimit) :

x < c → Order.succ x < c

source

theorem Cardinal.isSuccLimit_zero :

Order.IsSuccLimit 0

source

def Cardinal.sum {ι : Type u_1} (f : ι → Cardinal.{u_2}) :

Cardinal.{max u_2 u_1}

The indexed sum of cardinals is the cardinality of the indexed disjoint union, i.e. sigma type.

Equations

Cardinal.sum f = Cardinal.mk ((i : ι) × Quotient.out (f i))

Instances For

source

theorem Cardinal.le_sum {ι : Type u_1} (f : ι → Cardinal.{max u_1 u_2} ) (i : ι) :

f i ≤ Cardinal.sum f

source

@[simp]

theorem Cardinal.mk_sigma {ι : Type u_2} (f : ι → Type u_1) :

Cardinal.mk ((i : ι) × f i) = Cardinal.sum fun (i : ι) => Cardinal.mk (f i)

source

@[simp]

theorem Cardinal.sum_const (ι : Type u) (a : Cardinal.{v}) :

(Cardinal.sum fun (x : ι) => a) = Cardinal.lift.{v, u} (Cardinal.mk ι) * Cardinal.lift.{u, v} a

source

theorem Cardinal.sum_const' (ι : Type u) (a : Cardinal.{u}) :

(Cardinal.sum fun (x : ι) => a) = Cardinal.mk ι * a

source

@[simp]

theorem Cardinal.sum_add_distrib {ι : Type u_1} (f : ι → Cardinal.{u_2}) (g : ι → Cardinal.{u_2}) :

Cardinal.sum (f + g) = Cardinal.sum f + Cardinal.sum g

source

@[simp]

theorem Cardinal.sum_add_distrib' {ι : Type u_1} (f : ι → Cardinal.{u_2}) (g : ι → Cardinal.{u_2}) :

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

source

@[simp]

theorem Cardinal.lift_sum {ι : Type u} (f : ι → Cardinal.{v}) :

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

source

theorem Cardinal.sum_le_sum {ι : Type u_1} (f : ι → Cardinal.{u_2}) (g : ι → Cardinal.{u_2}) (H : ∀ (i : ι), f i ≤ g i) :

Cardinal.sum f ≤ Cardinal.sum g

source

theorem Cardinal.mk_le_mk_mul_of_mk_preimage_le {α : Type u} {β : Type u} {c : Cardinal.{u}} (f : α → β) (hf : ∀ (b : β), Cardinal.mk ↑(f ⁻¹' {b}) ≤ c) :

Cardinal.mk α ≤ Cardinal.mk β * c

source

theorem Cardinal.lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le {α : Type u} {β : Type v} {c : Cardinal.{max u v} } (f : α → β) (hf : ∀ (b : β), Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' {b})) ≤ c) :

Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β) * c

source

theorem Cardinal.bddAbove_range {ι : Type u} (f : ι → Cardinal.{max u v} ) :

BddAbove (Set.range f)

The range of an indexed cardinal function, whose outputs live in a higher universe than the inputs, is always bounded above.

source

instance Cardinal.instSmallElemIic (a : Cardinal.{u}) :

Small.{u, u + 1} ↑(Set.Iic a)

Equations

⋯ = ⋯

source

instance Cardinal.instSmallElemIio (a : Cardinal.{u}) :

Small.{u, u + 1} ↑(Set.Iio a)

Equations

⋯ = ⋯

source

theorem Cardinal.bddAbove_iff_small {s : Set Cardinal.{u}} :

BddAbove s ↔ Small.{u, u + 1} ↑s

A set of cardinals is bounded above iff it's small, i.e. it corresponds to a usual ZFC set.

source

theorem Cardinal.bddAbove_of_small (s : Set Cardinal.{u}) [h : Small.{u, u + 1} ↑s] :

BddAbove s

source

theorem Cardinal.bddAbove_image (f : Cardinal.{u} → Cardinal.{max u v} ) {s : Set Cardinal.{u}} (hs : BddAbove s) :

BddAbove (f '' s)

source

theorem Cardinal.bddAbove_range_comp {ι : Type u} {f : ι → Cardinal.{v}} (hf : BddAbove (Set.range f)) (g : Cardinal.{v} → Cardinal.{max v w} ) :

BddAbove (Set.range (g ∘ f))

source

theorem Cardinal.iSup_le_sum {ι : Type u_1} (f : ι → Cardinal.{max u_1 u_2} ) :

iSup f ≤ Cardinal.sum f

source

theorem Cardinal.sum_le_iSup_lift {ι : Type u} (f : ι → Cardinal.{max u v} ) :

Cardinal.sum f ≤ Cardinal.lift.{v, u} (Cardinal.mk ι) * iSup f

source

theorem Cardinal.sum_le_iSup {ι : Type u} (f : ι → Cardinal.{u}) :

Cardinal.sum f ≤ Cardinal.mk ι * iSup f

source

theorem Cardinal.sum_nat_eq_add_sum_succ (f : ℕ → Cardinal.{u}) :

Cardinal.sum f = f 0 + Cardinal.sum fun (i : ℕ) => f (i + 1)

source

theorem Cardinal.iSup_of_empty {ι : Sort u_1} (f : ι → Cardinal.{u_2}) [IsEmpty ι] :

iSup f = 0

A variant of ciSup_of_empty but with 0 on the RHS for convenience

source

theorem Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit {ι : Type u} (f : ι → Cardinal.{v}) (ω : Cardinal.{v}) (hω : ¬Order.IsSuccLimit ω) (h : ⨆ (i : ι), f i = ω) :

∃ (i : ι), f i = ω

source

theorem Cardinal.exists_eq_of_iSup_eq_of_not_isLimit {ι : Type u} [hι : Nonempty ι] (f : ι → Cardinal.{v}) (hf : BddAbove (Set.range f)) (ω : Cardinal.{v}) (hω : ¬ω.IsLimit) (h : ⨆ (i : ι), f i = ω) :

∃ (i : ι), f i = ω

source

@[simp]

theorem Cardinal.lift_mk_shrink (α : Type u) [Small.{v, u} α] :

Cardinal.lift.{max u w, v} (Cardinal.mk (Shrink.{v, u} α)) = Cardinal.lift.{max v w, u} (Cardinal.mk α)

source

@[simp]

theorem Cardinal.lift_mk_shrink' (α : Type u) [Small.{v, u} α] :

Cardinal.lift.{u, v} (Cardinal.mk (Shrink.{v, u} α)) = Cardinal.lift.{v, u} (Cardinal.mk α)

source

@[simp]

theorem Cardinal.lift_mk_shrink'' (α : Type (max u v)) [Small.{v, max u v} α] :

Cardinal.lift.{u, v} (Cardinal.mk (Shrink.{v, max u v} α)) = Cardinal.mk α

source

def Cardinal.prod {ι : Type u} (f : ι → Cardinal.{u_1}) :

Cardinal.{max u u_1}

The indexed product of cardinals is the cardinality of the Pi type (dependent product).

Equations

Cardinal.prod f = Cardinal.mk ((i : ι) → Quotient.out (f i))

Instances For

source

@[simp]

theorem Cardinal.mk_pi {ι : Type u} (α : ι → Type v) :

Cardinal.mk ((i : ι) → α i) = Cardinal.prod fun (i : ι) => Cardinal.mk (α i)

source

@[simp]

theorem Cardinal.prod_const (ι : Type u) (a : Cardinal.{v}) :

(Cardinal.prod fun (x : ι) => a) = Cardinal.lift.{u, v} a ^ Cardinal.lift.{v, u} (Cardinal.mk ι)

source

theorem Cardinal.prod_const' (ι : Type u) (a : Cardinal.{u}) :

(Cardinal.prod fun (x : ι) => a) = a ^ Cardinal.mk ι

source

theorem Cardinal.prod_le_prod {ι : Type u_1} (f : ι → Cardinal.{u_2}) (g : ι → Cardinal.{u_2}) (H : ∀ (i : ι), f i ≤ g i) :

Cardinal.prod f ≤ Cardinal.prod g

source

@[simp]

theorem Cardinal.prod_eq_zero {ι : Type u_1} (f : ι → Cardinal.{u}) :

Cardinal.prod f = 0 ↔ ∃ (i : ι), f i = 0

source

theorem Cardinal.prod_ne_zero {ι : Type u_1} (f : ι → Cardinal.{u_2}) :

Cardinal.prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0

source

@[simp]

theorem Cardinal.lift_prod {ι : Type u} (c : ι → Cardinal.{v}) :

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

source

theorem Cardinal.prod_eq_of_fintype {α : Type u} [h : Fintype α] (f : α → Cardinal.{v}) :

Cardinal.prod f = Cardinal.lift.{u, v} (∏ i : α, f i)

source

@[simp]

theorem Cardinal.lift_sInf (s : Set Cardinal.{v}) :

Cardinal.lift.{u, v} (sInf s) = sInf (Cardinal.lift.{u, v} '' s)

source

@[simp]

theorem Cardinal.lift_iInf {ι : Sort u_1} (f : ι → Cardinal.{v}) :

Cardinal.lift.{u, v} (iInf f) = ⨅ (i : ι), Cardinal.lift.{u, v} (f i)

source

theorem Cardinal.lift_down {a : Cardinal.{u}} {b : Cardinal.{max u v} } :

b ≤ Cardinal.lift.{v, u} a → ∃ (a' : Cardinal.{u}), Cardinal.lift.{v, u} a' = b

source

theorem Cardinal.le_lift_iff {a : Cardinal.{u}} {b : Cardinal.{max u v} } :

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

source

theorem Cardinal.lt_lift_iff {a : Cardinal.{u}} {b : Cardinal.{max u v} } :

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

source

@[simp]

theorem Cardinal.lift_succ (a : Cardinal.{u}) :

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

source

@[simp]

theorem Cardinal.lift_umax_eq {a : Cardinal.{u}} {b : Cardinal.{v}} :

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

source

@[simp]

theorem Cardinal.lift_min {a : Cardinal.{v}} {b : Cardinal.{v}} :

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

source

@[simp]

theorem Cardinal.lift_max {a : Cardinal.{v}} {b : Cardinal.{v}} :

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

source

theorem Cardinal.lift_sSup {s : Set Cardinal.{u_1}} (hs : BddAbove s) :

Cardinal.lift.{u, u_1} (sSup s) = sSup (Cardinal.lift.{u, u_1} '' s)

The lift of a supremum is the supremum of the lifts.

source

theorem Cardinal.lift_iSup {ι : Type v} {f : ι → Cardinal.{w}} (hf : BddAbove (Set.range f)) :

Cardinal.lift.{u, w} (iSup f) = ⨆ (i : ι), Cardinal.lift.{u, w} (f i)

The lift of a supremum is the supremum of the lifts.

source

theorem Cardinal.lift_iSup_le {ι : Type v} {f : ι → Cardinal.{w}} {t : Cardinal.{max u w} } (hf : BddAbove (Set.range f)) (w : ∀ (i : ι), Cardinal.lift.{u, w} (f i) ≤ t) :

Cardinal.lift.{u, w} (iSup f) ≤ t

To prove that the lift of a supremum is bounded by some cardinal t, it suffices to show that the lift of each cardinal is bounded by t.

source

@[simp]

theorem Cardinal.lift_iSup_le_iff {ι : Type v} {f : ι → Cardinal.{w}} (hf : BddAbove (Set.range f)) {t : Cardinal.{max u w} } :

Cardinal.lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), Cardinal.lift.{u, w} (f i) ≤ t

source

theorem Cardinal.lift_iSup_le_lift_iSup {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{w}} {f' : ι' → Cardinal.{w'}} (hf : BddAbove (Set.range f)) (hf' : BddAbove (Set.range f')) {g : ι → ι'} (h : ∀ (i : ι), Cardinal.lift.{w', w} (f i) ≤ Cardinal.lift.{w, w'} (f' (g i))) :

Cardinal.lift.{w', w} (iSup f) ≤ Cardinal.lift.{w, w'} (iSup f')

To prove an inequality between the lifts to a common universe of two different supremums, it suffices to show that the lift of each cardinal from the smaller supremum if bounded by the lift of some cardinal from the larger supremum.

source

theorem Cardinal.lift_iSup_le_lift_iSup' {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{v}} {f' : ι' → Cardinal.{v'}} (hf : BddAbove (Set.range f)) (hf' : BddAbove (Set.range f')) (g : ι → ι') (h : ∀ (i : ι), Cardinal.lift.{v', v} (f i) ≤ Cardinal.lift.{v, v'} (f' (g i))) :

Cardinal.lift.{v', v} (iSup f) ≤ Cardinal.lift.{v, v'} (iSup f')

A variant of lift_iSup_le_lift_iSup with universes specialized via w = v and w' = v'. This is sometimes necessary to avoid universe unification issues.

source

def Cardinal.aleph0 :

Cardinal.{u}

ℵ₀ is the smallest infinite cardinal.

Equations