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

Definition of cardinals

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.13) => Nonempty (α ≃ β), iseqv := Cardinal.isEquivalent.proof_1 }

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.3} = Quotient Cardinal.isEquivalent

def Cardinal.mk : Type u → Cardinal.{u}

The cardinal number of a type

Equations

• Cardinal.mk = Quotient.mk'

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

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

Equations

• Cardinal.canLiftCardinalType = ⋯

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

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₂

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₃

theorem Cardinal.induction_on_pi {ι : Type u} {p : (ι → Cardinal.{v}) → Prop} (f : ι → Cardinal.{v}) (h : ∀ (f : ι → Type v), p fun (i : ι) => Cardinal.mk (f i)) : p f

theorem Cardinal.eq {α : Type u} {β : Type u} : Cardinal.mk α = Cardinal.mk β ↔ Nonempty (α ≃ β)

@[simp]

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

@[simp]

theorem Cardinal.mk_out (c : Cardinal.{u_1}) : Cardinal.mk (Quotient.out c) = c

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

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

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

Alias of Cardinal.mk_congr.

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 ⋯

@[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 α)

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 ⋯

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.28}) => Quotient.liftOn₂ q₁ q₂ (fun (α β : Type ?u.28) => Nonempty (α ↪ β)) Cardinal.instLE.proof_1 }

instance Cardinal.partialOrder : PartialOrder Cardinal.{u}

Equations

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

instance Cardinal.linearOrder : LinearOrder Cardinal.{u}

Equations

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

theorem Cardinal.le_def (α : Type u) (β : Type u) : Cardinal.mk α ≤ Cardinal.mk β ↔ Nonempty (α ↪ β)

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

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

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

theorem Cardinal.le_mk_iff_exists_set {c : Cardinal.{u}} {α : Type u} : c ≤ Cardinal.mk α ↔ ∃ (p : Set α), Cardinal.mk ↑p = c

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

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

Lifting cardinals to a higher universe

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.14, ?u.13} c = Cardinal.map ULift.{?u.14, ?u.13} (fun (x x_1 : Type ?u.13) (e : x ≃ x_1) => Equiv.ulift.trans (e.trans Equiv.ulift.symm)) c

@[simp]

theorem Cardinal.mk_uLift (α : Type u) : Cardinal.mk (ULift.{v, u} α) = Cardinal.lift.{v, u} (Cardinal.mk α)

@[simp]

theorem Cardinal.lift_umax : Cardinal.lift.{max u v, u} = Cardinal.lift.{v, u}

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

@[simp]

theorem Cardinal.lift_umax' : Cardinal.lift.{max v u, u} = Cardinal.lift.{v, u}

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

@[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.

@[simp]

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

A cardinal lifted to the same universe equals itself.

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

A cardinal lifted to the zero universe equals itself.

@[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

@[simp]

theorem Cardinal.mk_preimage_down {α : Type u} {s : Set α} : Cardinal.mk ↑(ULift.down ⁻¹' s) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)

theorem Cardinal.out_embedding {c : Cardinal.{u_1}} {c' : Cardinal.{u_1}} : c ≤ c' ↔ Nonempty (Quotient.out c ↪ Quotient.out c')

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 (α ↪ β)

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.

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 (α ≃ β)

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.

@[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 α)

@[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 α)

@[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 α

@[simp]

theorem Cardinal.liftInitialSeg_toFun (c : Cardinal.{u}) : Cardinal.liftInitialSeg c = Cardinal.lift.{v, u} c

def Cardinal.liftInitialSeg : (fun (x1 x2 : Cardinal.{u}) => x1 < x2) ≼i fun (x1 x2 : Cardinal.{max u v} ) => x1 < x2

Cardinal.lift as an InitialSeg.

Equations

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

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

@[deprecated Cardinal.mem_range_lift_of_le]

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

@[deprecated Cardinal.liftInitialSeg]

def Cardinal.liftOrderEmbedding : Cardinal.{v} ↪o Cardinal.{max v u}

Cardinal.lift as an OrderEmbedding.

Equations

• Cardinal.liftOrderEmbedding = Cardinal.liftInitialSeg.toOrderEmbedding

theorem Cardinal.lift_injective : Function.Injective Cardinal.lift.{u, v}

@[simp]

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

@[simp]

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

@[simp]

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

theorem Cardinal.lift_strictMono : StrictMono Cardinal.lift.{u_2, u_1}

theorem Cardinal.lift_monotone : Monotone Cardinal.lift.{u_2, u_1}

@[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)

@[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)

@[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

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

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

Basic cardinals

instance Cardinal.instZero : Zero Cardinal.{u}

Equations

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

instance Cardinal.instInhabited : Inhabited Cardinal.{u}

Equations

• Cardinal.instInhabited = { default := 0 }

@[simp]

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

@[simp]

theorem Cardinal.lift_zero : Cardinal.lift.{u_2, u_1} 0 = 0

@[simp]

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

theorem Cardinal.mk_eq_zero_iff {α : Type u} : Cardinal.mk α = 0 ↔ IsEmpty α

theorem Cardinal.mk_ne_zero_iff {α : Type u} : Cardinal.mk α ≠ 0 ↔ Nonempty α

@[simp]

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

instance Cardinal.instOne : One Cardinal.{u}

Equations

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

instance Cardinal.instNontrivial : Nontrivial Cardinal.{u}

Equations

• Cardinal.instNontrivial = ⋯

theorem Cardinal.mk_eq_one (α : Type u) [Subsingleton α] [Nonempty α] : Cardinal.mk α = 1

theorem Cardinal.le_one_iff_subsingleton {α : Type u} : Cardinal.mk α ≤ 1 ↔ Subsingleton α

@[simp]

theorem Cardinal.mk_le_one_iff_set_subsingleton {α : Type u} {s : Set α} : Cardinal.mk ↑s ≤ 1 ↔ s.Subsingleton

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.

instance Cardinal.instAdd : Add Cardinal.{u}

Equations

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

theorem Cardinal.add_def (α : Type u) (β : Type u) : Cardinal.mk α + Cardinal.mk β = Cardinal.mk (α ⊕ β)

instance Cardinal.instNatCast : NatCast Cardinal.{u}

Equations

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

@[simp]

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

@[simp]

theorem Cardinal.mk_option {α : Type u} : Cardinal.mk (Option α) = Cardinal.mk α + 1

@[simp]

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

@[simp]

theorem Cardinal.mk_fintype (α : Type u) [h : Fintype α] : Cardinal.mk α = ↑(Fintype.card α)

instance Cardinal.instMul : Mul Cardinal.{u}

Equations

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

theorem Cardinal.mul_def (α : Type u) (β : Type u) : Cardinal.mk α * Cardinal.mk β = Cardinal.mk (α × β)

@[simp]

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

instance Cardinal.instPowCardinal : Pow Cardinal.{u} Cardinal.{u}

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

Equations

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

theorem Cardinal.power_def (α : Type u) (β : Type u) : Cardinal.mk α ^ Cardinal.mk β = Cardinal.mk (β → α)

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

@[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

@[simp]

theorem Cardinal.power_zero (a : Cardinal.{u_1}) : a ^ 0 = 1

@[simp]

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

theorem Cardinal.power_add (a : Cardinal.{u_1}) (b : Cardinal.{u_1}) (c : Cardinal.{u_1}) : a ^ (b + c) = a ^ b * a ^ c

instance Cardinal.commSemiring : CommSemiring Cardinal.{u}

Equations

• Cardinal.commSemiring = CommSemiring.mk Cardinal.commSemiring.proof_16

@[simp]

theorem Cardinal.one_power {a : Cardinal.{u_1}} : 1 ^ a = 1

theorem Cardinal.mk_bool : Cardinal.mk Bool = 2

theorem Cardinal.mk_Prop : Cardinal.mk Prop = 2

@[simp]

theorem Cardinal.zero_power {a : Cardinal.{u_1}} : a ≠ 0 → 0 ^ a = 0

theorem Cardinal.power_ne_zero {a : Cardinal.{u_1}} (b : Cardinal.{u_1}) : a ≠ 0 → a ^ b ≠ 0

theorem Cardinal.mul_power {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} : (a * b) ^ c = a ^ c * b ^ c

theorem Cardinal.power_mul {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} : a ^ (b * c) = (a ^ b) ^ c

@[simp]

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

@[deprecated Cardinal.power_natCast]

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

Alias of Cardinal.power_natCast.

@[simp]

theorem Cardinal.lift_one : Cardinal.lift.{u_2, u_1} 1 = 1

@[simp]

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

@[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

@[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

theorem Cardinal.lift_two : Cardinal.lift.{u, v} 2 = 2

@[simp]

theorem Cardinal.mk_set {α : Type u} : Cardinal.mk (Set α) = 2 ^ Cardinal.mk α

@[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.

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

Order properties

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

instance Cardinal.add_covariantClass : CovariantClass Cardinal.{u_1} Cardinal.{u_1} (fun (x1 x2 : Cardinal.{u_1}) => x1 + x2) fun (x1 x2 : Cardinal.{u_1}) => x1 ≤ x2

Equations

• Cardinal.add_covariantClass = ⋯

instance Cardinal.add_swap_covariantClass : CovariantClass Cardinal.{u_1} Cardinal.{u_1} (Function.swap fun (x1 x2 : Cardinal.{u_1}) => x1 + x2) fun (x1 x2 : Cardinal.{u_1}) => x1 ≤ x2

Equations

• Cardinal.add_swap_covariantClass = ⋯

instance Cardinal.canonicallyOrderedCommSemiring : CanonicallyOrderedCommSemiring Cardinal.{u}

Equations

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

instance Cardinal.instCanonicallyLinearOrderedAddCommMonoid : CanonicallyLinearOrderedAddCommMonoid Cardinal.{u}

Equations

• Cardinal.instCanonicallyLinearOrderedAddCommMonoid = CanonicallyLinearOrderedAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance Cardinal.instCanonicallyOrderedAddCommMonoid : CanonicallyOrderedAddCommMonoid Cardinal.{u}

Equations

• Cardinal.instCanonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk (@Cardinal.instCanonicallyOrderedAddCommMonoid.proof_1) Cardinal.instCanonicallyOrderedAddCommMonoid.proof_2

instance Cardinal.instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero Cardinal.{u}

Equations

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

instance Cardinal.instCommMonoidWithZero : CommMonoidWithZero Cardinal.{u}

Equations

• Cardinal.instCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯

instance Cardinal.instCommMonoid : CommMonoid Cardinal.{u}

Equations

• Cardinal.instCommMonoid = CommMonoid.mk ⋯

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

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

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

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

Cantor's theorem

instance Cardinal.instNoMaxOrder : NoMaxOrder Cardinal.{u}

Equations

• Cardinal.instNoMaxOrder = ⋯

instance Cardinal.instDistribLattice : DistribLattice Cardinal.{u}

Equations

• Cardinal.instDistribLattice = inferInstance

theorem Cardinal.one_lt_iff_nontrivial {α : Type u} : 1 < Cardinal.mk α ↔ Nontrivial α

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

theorem Cardinal.power_le_power_right {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} : a ≤ b → a ^ c ≤ b ^ c

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

theorem Cardinal.lt_wf : WellFounded fun (x1 x2 : Cardinal.{u}) => x1 < x2

instance Cardinal.instWellFoundedRelation : WellFoundedRelation Cardinal.{u}

Equations

• Cardinal.instWellFoundedRelation = { rel := fun (x1 x2 : Cardinal.{?u.5}) => x1 < x2, wf := Cardinal.lt_wf }

instance Cardinal.instWellFoundedLT : WellFoundedLT Cardinal.{u}

Equations

• Cardinal.instWellFoundedLT = ⋯

instance Cardinal.wo : IsWellOrder Cardinal.{u} fun (x1 x2 : Cardinal.{u}) => x1 < x2

Equations

• Cardinal.wo = ⋯

instance Cardinal.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot Cardinal.{u_1}

Equations

• Cardinal.instConditionallyCompleteLinearOrderBot = WellFoundedLT.conditionallyCompleteLinearOrderBot Cardinal.{?u.3}

@[simp]

theorem Cardinal.sInf_empty : sInf ∅ = 0

theorem Cardinal.sInf_eq_zero_iff {s : Set Cardinal.{u_1}} : sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0

theorem Cardinal.iInf_eq_zero_iff {ι : Sort u_1} {f : ι → Cardinal.{u_2}} : ⨅ (i : ι), f i = 0 ↔ IsEmpty ι ∨ ∃ (i : ι), f i = 0

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

@[simp]

theorem Cardinal.lift_sInf (s : Set Cardinal.{v}) : Cardinal.lift.{u, v} (sInf s) = sInf (Cardinal.lift.{u, v} '' s)

@[simp]

theorem Cardinal.lift_iInf {ι : Sort u_1} (f : ι → Cardinal.{v}) : Cardinal.lift.{u, v} (iInf f) = ⨅ (i : ι), Cardinal.lift.{u, v} (f i)

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 = ConditionallyCompleteLinearOrder.toSuccOrder

theorem Cardinal.succ_def (c : Cardinal.{u_1}) : Order.succ c = sInf {c' : Cardinal.{u_1} | c < c'}

theorem Cardinal.succ_pos (c : Cardinal.{u_1}) : 0 < Order.succ c

theorem Cardinal.succ_ne_zero (c : Cardinal.{u_1}) : Order.succ c ≠ 0

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

@[simp]

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

@[deprecated Order.IsSuccLimit]

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. Deprecated. Use Order.IsSuccLimit instead.

Equations

• c.IsLimit = (c ≠ 0 ∧ Order.IsSuccPrelimit c)

theorem Cardinal.ne_zero_of_isSuccLimit {c : ℕ} (h : Order.IsSuccLimit c) : c ≠ 0

theorem Cardinal.isSuccPrelimit_zero : Order.IsSuccPrelimit 0

theorem Cardinal.isSuccLimit_iff {c : Cardinal.{u_1}} : Order.IsSuccLimit c ↔ c ≠ 0 ∧ Order.IsSuccPrelimit c

@[deprecated Order.IsSuccLimit.isSuccPrelimit]

theorem Cardinal.IsLimit.isSuccPrelimit {c : Cardinal.{u_1}} (h : c.IsLimit) : Order.IsSuccPrelimit c

@[deprecated Cardinal.ne_zero_of_isSuccLimit]

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

@[deprecated Cardinal.IsLimit.isSuccPrelimit]

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

Alias of Cardinal.IsLimit.isSuccPrelimit.

@[deprecated Order.IsSuccLimit.succ_lt]

theorem Cardinal.IsLimit.succ_lt {x : Cardinal.{u_1}} {c : Cardinal.{u_1}} (h : c.IsLimit) : x < c → Order.succ x < c

@[deprecated Cardinal.isSuccPrelimit_zero]

theorem Cardinal.isSuccLimit_zero : Order.IsSuccPrelimit 0

Alias of Cardinal.isSuccPrelimit_zero.

Indexed cardinal sum

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

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

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

@[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)

theorem Cardinal.mk_sigma_congr_lift {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι') (h : ∀ (i : ι), Cardinal.lift.{w', w} (Cardinal.mk (f i)) = Cardinal.lift.{w, w'} (Cardinal.mk (g (e i)))) : Cardinal.lift.{max v' w', max w v} (Cardinal.mk ((i : ι) × f i)) = Cardinal.lift.{max v w, max w' v'} (Cardinal.mk ((i : ι') × g i))

theorem Cardinal.mk_sigma_congr {ι : Type u} {ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι') (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) : Cardinal.mk ((i : ι) × f i) = Cardinal.mk ((i : ι') × g i)

theorem Cardinal.mk_sigma_congr' {ι : Type u} {ι' : Type v} {f : ι → Type (max w u v)} {g : ι' → Type (max w u v)} (e : ι ≃ ι') (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) : Cardinal.mk ((i : ι) × f i) = Cardinal.mk ((i : ι') × g i)

Similar to mk_sigma_congr with indexing types in different universes. This is not a strict generalization.

theorem Cardinal.mk_sigma_congrRight {ι : Type u} {f : ι → Type v} {g : ι → Type v} (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g i)) : Cardinal.mk ((i : ι) × f i) = Cardinal.mk ((i : ι) × g i)

theorem Cardinal.mk_psigma_congrRight {ι : Type u} {f : ι → Type v} {g : ι → Type v} (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g i)) : Cardinal.mk ((i : ι) ×' f i) = Cardinal.mk ((i : ι) ×' g i)

theorem Cardinal.mk_psigma_congrRight_prop {ι : Prop} {f : ι → Type v} {g : ι → Type v} (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g i)) : Cardinal.mk ((i : ι) ×' f i) = Cardinal.mk ((i : ι) ×' g i)

theorem Cardinal.mk_sigma_arrow {ι : Type u_3} (α : Type u_1) (f : ι → Type u_2) : Cardinal.mk (Sigma f → α) = Cardinal.mk ((i : ι) → f i → α)

@[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

theorem Cardinal.sum_const' (ι : Type u) (a : Cardinal.{u}) : (Cardinal.sum fun (x : ι) => a) = Cardinal.mk ι * a

@[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

@[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

@[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)

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

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

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

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

Well-ordering theorem

theorem nonempty_embedding_to_cardinal {α : Type u} : Nonempty (α ↪ Cardinal.{u})

def embeddingToCardinal {α : Type u} : α ↪ Cardinal.{u}

An embedding of any type to the set of cardinals in its universe.

Equations

• embeddingToCardinal = Classical.choice ⋯

def WellOrderingRel {α : Type u} : α → α → Prop

Any type can be endowed with a well order, obtained by pulling back the well order over cardinals by some embedding.

Equations

• WellOrderingRel = ⇑embeddingToCardinal ⁻¹'o fun (x1 x2 : Cardinal.{?u.20}) => x1 < x2

instance WellOrderingRel.isWellOrder {α : Type u} : IsWellOrder α WellOrderingRel

Equations

• ⋯ = ⋯

instance IsWellOrder.subtype_nonempty {α : Type u} : Nonempty { r : α → α → Prop // IsWellOrder α r }

Equations

• ⋯ = ⋯

theorem exists_wellOrder (α : Type u) : ∃ (x : LinearOrder α), WellFoundedLT α

The well-ordering theorem (or Zermelo's theorem): every type has a well-order

Small sets of cardinals

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.

instance Cardinal.small_Iic (a : Cardinal.{u}) : Small.{u, u + 1} ↑(Set.Iic a)

Equations

• ⋯ = ⋯

instance Cardinal.small_Iio (a : Cardinal.{u}) : Small.{u, u + 1} ↑(Set.Iio a)

Equations

• ⋯ = ⋯

instance Cardinal.small_Icc (a : Cardinal.{u}) (b : Cardinal.{u}) : Small.{u, u + 1} ↑(Set.Icc a b)

Equations

• ⋯ = ⋯

instance Cardinal.small_Ico (a : Cardinal.{u}) (b : Cardinal.{u}) : Small.{u, u + 1} ↑(Set.Ico a b)

Equations

• ⋯ = ⋯

instance Cardinal.small_Ioc (a : Cardinal.{u}) (b : Cardinal.{u}) : Small.{u, u + 1} ↑(Set.Ioc a b)

Equations

• ⋯ = ⋯

instance Cardinal.small_Ioo (a : Cardinal.{u}) (b : Cardinal.{u}) : Small.{u, u + 1} ↑(Set.Ioo a b)

Equations

• ⋯ = ⋯

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.

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

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

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

Bounds on suprema

theorem Cardinal.sum_le_iSup_lift {ι : Type u} (f : ι → Cardinal.{max u v} ) : Cardinal.sum f ≤ Cardinal.lift.{v, u} (Cardinal.mk ι) * iSup f

theorem Cardinal.sum_le_iSup {ι : Type u} (f : ι → Cardinal.{u}) : Cardinal.sum f ≤ Cardinal.mk ι * iSup f

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.

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.

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.

@[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

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.

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.

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

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

@[deprecated Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit]

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 = ω

Indexed cardinal prod

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

@[simp]

theorem Cardinal.mk_pi {ι : Type u} (α : ι → Type v) : Cardinal.mk ((i : ι) → α i) = Cardinal.prod fun (i : ι) => Cardinal.mk (α i)

theorem Cardinal.mk_pi_congr_lift {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι') (h : ∀ (i : ι), Cardinal.lift.{w', w} (Cardinal.mk (f i)) = Cardinal.lift.{w, w'} (Cardinal.mk (g (e i)))) : Cardinal.lift.{max v' w', max v w} (Cardinal.mk ((i : ι) → f i)) = Cardinal.lift.{max v w, max v' w'} (Cardinal.mk ((i : ι') → g i))

theorem Cardinal.mk_pi_congr {ι : Type u} {ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι') (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) : Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι') → g i)

theorem Cardinal.mk_pi_congr_prop {ι : Prop} {ι' : Prop} {f : ι → Type v} {g : ι' → Type v} (e : ι ↔ ι') (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g ⋯)) : Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι') → g i)

theorem Cardinal.mk_pi_congr' {ι : Type u} {ι' : Type v} {f : ι → Type (max w u v)} {g : ι' → Type (max w u v)} (e : ι ≃ ι') (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) : Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι') → g i)

Similar to mk_pi_congr with indexing types in different universes. This is not a strict generalization.

theorem Cardinal.mk_pi_congrRight {ι : Type u} {f : ι → Type v} {g : ι → Type v} (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g i)) : Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι) → g i)

theorem Cardinal.mk_pi_congrRight_prop {ι : Prop} {f : ι → Type v} {g : ι → Type v} (h : ∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g i)) : Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι) → g i)

@[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 ι)

theorem Cardinal.prod_const' (ι : Type u) (a : Cardinal.{u}) : (Cardinal.prod fun (x : ι) => a) = a ^ Cardinal.mk ι

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

@[simp]

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

theorem Cardinal.prod_ne_zero {ι : Type u_1} (f : ι → Cardinal.{u_2}) : Cardinal.prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0

theorem Cardinal.power_sum {ι : Type u_1} (a : Cardinal.{max u_1 u_2} ) (f : ι → Cardinal.{max u_1 u_2} ) : a ^ Cardinal.sum f = Cardinal.prod fun (i : ι) => a ^ f i

@[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)

theorem Cardinal.prod_eq_of_fintype {α : Type u} [h : Fintype α] (f : α → Cardinal.{v}) : Cardinal.prod f = Cardinal.lift.{u, v} (∏ i : α, f i)

theorem Cardinal.sum_lt_prod {ι : Type u_1} (f : ι → Cardinal.{u_2}) (g : ι → Cardinal.{u_2}) (H : ∀ (i : ι), f i < g i) : Cardinal.sum f < Cardinal.prod g

König's theorem

The first infinite cardinal aleph0

def Cardinal.aleph0 : Cardinal.{u}

ℵ₀ is the smallest infinite cardinal.

Equations

• Cardinal.aleph0 = Cardinal.lift.{?u.1, 0} (Cardinal.mk ℕ)

def Cardinal.termℵ₀ : Lean.ParserDescr

ℵ₀ is the smallest infinite cardinal.

Equations

• Cardinal.termℵ₀ = Lean.ParserDescr.node `Cardinal.termℵ₀ 1024 (Lean.ParserDescr.symbol "ℵ₀")

theorem Cardinal.mk_nat : Cardinal.mk ℕ = Cardinal.aleph0

theorem Cardinal.aleph0_ne_zero : Cardinal.aleph0 ≠ 0

theorem Cardinal.aleph0_pos : 0 < Cardinal.aleph0

@[simp]

theorem Cardinal.lift_aleph0 : Cardinal.lift.{u_1, u_2} Cardinal.aleph0 = Cardinal.aleph0

@[simp]

theorem Cardinal.aleph0_le_lift {c : Cardinal.{u}} : Cardinal.aleph0 ≤ Cardinal.lift.{v, u} c ↔ Cardinal.aleph0 ≤ c

@[simp]

theorem Cardinal.lift_le_aleph0 {c : Cardinal.{u}} : Cardinal.lift.{v, u} c ≤ Cardinal.aleph0 ↔ c ≤ Cardinal.aleph0

@[simp]

theorem Cardinal.aleph0_lt_lift {c : Cardinal.{u}} : Cardinal.aleph0 < Cardinal.lift.{v, u} c ↔ Cardinal.aleph0 < c

@[simp]

theorem Cardinal.lift_lt_aleph0 {c : Cardinal.{u}} : Cardinal.lift.{v, u} c < Cardinal.aleph0 ↔ c < Cardinal.aleph0

@[simp]

theorem Cardinal.aleph0_eq_lift {c : Cardinal.{u}} : Cardinal.aleph0 = Cardinal.lift.{v, u} c ↔ Cardinal.aleph0 = c

@[simp]

theorem Cardinal.lift_eq_aleph0 {c : Cardinal.{u}} : Cardinal.lift.{v, u} c = Cardinal.aleph0 ↔ c = Cardinal.aleph0

Properties about the cast from ℕ

theorem Cardinal.mk_fin (n : ℕ) : Cardinal.mk (Fin n) = ↑n

@[simp]

theorem Cardinal.lift_natCast (n : ℕ) : Cardinal.lift.{u, v} ↑n = ↑n

@[simp]

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

@[simp]

theorem Cardinal.lift_eq_nat_iff {a : Cardinal.{u}} {n : ℕ} : Cardinal.lift.{v, u} a = ↑n ↔ a = ↑n

@[simp]

theorem Cardinal.lift_eq_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : Cardinal.lift.{v, u} a = OfNat.ofNat n ↔ a = OfNat.ofNat n

@[simp]

theorem Cardinal.nat_eq_lift_iff {n : ℕ} {a : Cardinal.{u}} : ↑n = Cardinal.lift.{v, u} a ↔ ↑n = a

@[simp]

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

@[simp]

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

@[simp]

theorem Cardinal.ofNat_eq_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n = Cardinal.lift.{v, u} a ↔ OfNat.ofNat n = a

@[simp]

theorem Cardinal.lift_le_nat_iff {a : Cardinal.{u}} {n : ℕ} : Cardinal.lift.{v, u} a ≤ ↑n ↔ a ≤ ↑n

@[simp]

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

@[simp]

theorem Cardinal.lift_le_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : Cardinal.lift.{v, u} a ≤ OfNat.ofNat n ↔ a ≤ OfNat.ofNat n

@[simp]

theorem Cardinal.nat_le_lift_iff {n : ℕ} {a : Cardinal.{u}} : ↑n ≤ Cardinal.lift.{v, u} a ↔ ↑n ≤ a

@[simp]

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

@[simp]

theorem Cardinal.ofNat_le_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n ≤ Cardinal.lift.{v, u} a ↔ OfNat.ofNat n ≤ a

@[simp]

theorem Cardinal.lift_lt_nat_iff {a : Cardinal.{u}} {n : ℕ} : Cardinal.lift.{v, u} a < ↑n ↔ a < ↑n

@[simp]

theorem Cardinal.lift_lt_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : Cardinal.lift.{v, u} a < OfNat.ofNat n ↔ a < OfNat.ofNat n

@[simp]

theorem Cardinal.nat_lt_lift_iff {n : ℕ} {a : Cardinal.{u}} : ↑n < Cardinal.lift.{v, u} a ↔ ↑n < a

@[simp]

theorem Cardinal.zero_lt_lift_iff {a : Cardinal.{u}} : 0 < Cardinal.lift.{v, u} a ↔ 0 < a

@[simp]

theorem Cardinal.one_lt_lift_iff {a : Cardinal.{u}} : 1 < Cardinal.lift.{v, u} a ↔ 1 < a

@[simp]

theorem Cardinal.ofNat_lt_lift_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n < Cardinal.lift.{v, u} a ↔ OfNat.ofNat n < a

theorem Cardinal.lift_mk_fin (n : ℕ) : Cardinal.lift.{u_1, 0} (Cardinal.mk (Fin n)) = ↑n

theorem Cardinal.mk_coe_finset {α : Type u} {s : Finset α} : Cardinal.mk { x : α // x ∈ s } = ↑s.card

theorem Cardinal.mk_finset_of_fintype {α : Type u} [Fintype α] : Cardinal.mk (Finset α) = 2 ^ Fintype.card α

theorem Cardinal.card_le_of_finset {α : Type u_1} (s : Finset α) : ↑s.card ≤ Cardinal.mk α

instance Cardinal.instCharZero : CharZero Cardinal.{u_1}

Equations

• Cardinal.instCharZero = ⋯

@[deprecated Nat.cast_le]

theorem Cardinal.natCast_le {m : ℕ} {n : ℕ} : ↑m ≤ ↑n ↔ m ≤ n

@[deprecated Nat.cast_lt]

theorem Cardinal.natCast_lt {m : ℕ} {n : ℕ} : ↑m < ↑n ↔ m < n

@[deprecated Nat.cast_inj]

theorem Cardinal.natCast_inj {m : ℕ} {n : ℕ} : ↑m = ↑n ↔ m = n

@[deprecated Nat.cast_injective]

theorem Cardinal.natCast_injective : Function.Injective Nat.cast

@[deprecated Nat.cast_pow]

theorem Cardinal.natCast_pow {m : ℕ} {n : ℕ} : ↑(m ^ n) = ↑m ^ ↑n

theorem Cardinal.nat_succ (n : ℕ) : ↑n.succ = Order.succ ↑n

theorem Cardinal.succ_natCast (n : ℕ) : Order.succ ↑n = ↑n + 1

theorem Cardinal.natCast_add_one_le_iff {n : ℕ} {c : Cardinal.{u_1}} : ↑n + 1 ≤ c ↔ ↑n < c

theorem Cardinal.two_le_iff_one_lt {c : Cardinal.{u_1}} : 2 ≤ c ↔ 1 < c

@[simp]

theorem Cardinal.succ_zero : Order.succ 0 = 1

theorem Cardinal.one_lt_two : 1 < 2

theorem Cardinal.exists_finset_le_card (α : Type u_1) (n : ℕ) (h : ↑n ≤ Cardinal.mk α) : ∃ (s : Finset α), n ≤ s.card

theorem Cardinal.card_le_of {α : Type u} {n : ℕ} (H : ∀ (s : Finset α), s.card ≤ n) : Cardinal.mk α ≤ ↑n

theorem Cardinal.cantor' (a : Cardinal.{u_1}) {b : Cardinal.{u_1}} (hb : 1 < b) : a < b ^ a

theorem Cardinal.one_le_iff_pos {c : Cardinal.{u_1}} : 1 ≤ c ↔ 0 < c

theorem Cardinal.one_le_iff_ne_zero {c : Cardinal.{u_1}} : 1 ≤ c ↔ c ≠ 0

@[simp]

theorem Cardinal.lt_one_iff_zero {c : Cardinal.{u_1}} : c < 1 ↔ c = 0

Properties about aleph0

theorem Cardinal.nat_lt_aleph0 (n : ℕ) : ↑n < Cardinal.aleph0

@[simp]

theorem Cardinal.one_lt_aleph0 : 1 < Cardinal.aleph0

theorem Cardinal.one_le_aleph0 : 1 ≤ Cardinal.aleph0

theorem Cardinal.lt_aleph0 {c : Cardinal.{u_1}} : c < Cardinal.aleph0 ↔ ∃ (n : ℕ), c = ↑n

theorem Cardinal.succ_eq_of_lt_aleph0 {c : Cardinal.{u_1}} (h : c < Cardinal.aleph0) : Order.succ c = c + 1

theorem Cardinal.aleph0_le {c : Cardinal.{u_1}} : Cardinal.aleph0 ≤ c ↔ ∀ (n : ℕ), ↑n ≤ c

theorem Cardinal.isSuccPrelimit_aleph0 : Order.IsSuccPrelimit Cardinal.aleph0

theorem Cardinal.isSuccLimit_aleph0 : Order.IsSuccLimit Cardinal.aleph0

theorem Cardinal.not_isSuccLimit_natCast (n : ℕ) : ¬Order.IsSuccLimit ↑n

theorem Cardinal.not_isSuccLimit_of_lt_aleph0 {c : Cardinal.{u_1}} (h : c < Cardinal.aleph0) : ¬Order.IsSuccLimit c

theorem Cardinal.aleph0_le_of_isSuccLimit {c : Cardinal.{u_1}} (h : Order.IsSuccLimit c) : Cardinal.aleph0 ≤ c

@[deprecated Cardinal.isSuccLimit_aleph0]

theorem Cardinal.isLimit_aleph0 : Cardinal.aleph0.IsLimit

@[deprecated Cardinal.not_isSuccLimit_natCast]

theorem Cardinal.not_isLimit_natCast (n : ℕ) : ¬(↑n).IsLimit

@[deprecated Cardinal.aleph0_le_of_isSuccLimit]

theorem Cardinal.IsLimit.aleph0_le {c : Cardinal.{u_1}} (h : c.IsLimit) : Cardinal.aleph0 ≤ c

theorem Cardinal.exists_eq_natCast_of_iSup_eq {ι : Type u} [Nonempty ι] (f : ι → Cardinal.{v}) (hf : BddAbove (Set.range f)) (n : ℕ) (h : ⨆ (i : ι), f i = ↑n) : ∃ (i : ι), f i = ↑n

@[simp]

theorem Cardinal.range_natCast : Set.range Nat.cast = Set.Iio Cardinal.aleph0

theorem Cardinal.mk_eq_nat_iff {α : Type u} {n : ℕ} : Cardinal.mk α = ↑n ↔ Nonempty (α ≃ Fin n)

theorem Cardinal.lt_aleph0_iff_finite {α : Type u} : Cardinal.mk α < Cardinal.aleph0 ↔ Finite α

theorem Cardinal.lt_aleph0_iff_fintype {α : Type u} : Cardinal.mk α < Cardinal.aleph0 ↔ Nonempty (Fintype α)

theorem Cardinal.lt_aleph0_of_finite (α : Type u) [Finite α] : Cardinal.mk α < Cardinal.aleph0

theorem Cardinal.lt_aleph0_iff_set_finite {α : Type u} {S : Set α} : Cardinal.mk ↑S < Cardinal.aleph0 ↔ S.Finite

theorem Set.Finite.lt_aleph0 {α : Type u} {S : Set α} : S.Finite → Cardinal.mk ↑S < Cardinal.aleph0

Alias of the reverse direction of Cardinal.lt_aleph0_iff_set_finite.

@[simp]

theorem Cardinal.lt_aleph0_iff_subtype_finite {α : Type u} {p : α → Prop} : Cardinal.mk { x : α // p x } < Cardinal.aleph0 ↔ {x : α | p x}.Finite

theorem Cardinal.mk_le_aleph0_iff {α : Type u} : Cardinal.mk α ≤ Cardinal.aleph0 ↔ Countable α

@[simp]

theorem Cardinal.mk_le_aleph0 {α : Type u} [Countable α] : Cardinal.mk α ≤ Cardinal.aleph0

theorem Cardinal.le_aleph0_iff_set_countable {α : Type u} {s : Set α} : Cardinal.mk ↑s ≤ Cardinal.aleph0 ↔ s.Countable

theorem Set.Countable.le_aleph0 {α : Type u} {s : Set α} : s.Countable → Cardinal.mk ↑s ≤ Cardinal.aleph0

Alias of the reverse direction of Cardinal.le_aleph0_iff_set_countable.

@[simp]

theorem Cardinal.le_aleph0_iff_subtype_countable {α : Type u} {p : α → Prop} : Cardinal.mk { x : α // p x } ≤ Cardinal.aleph0 ↔ {x : α | p x}.Countable

instance Cardinal.canLiftCardinalNat : CanLift Cardinal.{u_1} ℕ Nat.cast fun (x : Cardinal.{u_1}) => x < Cardinal.aleph0

Equations

• Cardinal.canLiftCardinalNat = ⋯

theorem Cardinal.add_lt_aleph0 {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : a < Cardinal.aleph0) (hb : b < Cardinal.aleph0) : a + b < Cardinal.aleph0

theorem Cardinal.add_lt_aleph0_iff {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} : a + b < Cardinal.aleph0 ↔ a < Cardinal.aleph0 ∧ b < Cardinal.aleph0

theorem Cardinal.aleph0_le_add_iff {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} : Cardinal.aleph0 ≤ a + b ↔ Cardinal.aleph0 ≤ a ∨ Cardinal.aleph0 ≤ b

theorem Cardinal.nsmul_lt_aleph0_iff {n : ℕ} {a : Cardinal.{u_1}} : n • a < Cardinal.aleph0 ↔ n = 0 ∨ a < Cardinal.aleph0

See also Cardinal.nsmul_lt_aleph0_iff_of_ne_zero if you already have n ≠ 0.

theorem Cardinal.nsmul_lt_aleph0_iff_of_ne_zero {n : ℕ} {a : Cardinal.{u_1}} (h : n ≠ 0) : n • a < Cardinal.aleph0 ↔ a < Cardinal.aleph0

See also Cardinal.nsmul_lt_aleph0_iff for a hypothesis-free version.

theorem Cardinal.mul_lt_aleph0 {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : a < Cardinal.aleph0) (hb : b < Cardinal.aleph0) : a * b < Cardinal.aleph0

theorem Cardinal.mul_lt_aleph0_iff {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} : a * b < Cardinal.aleph0 ↔ a = 0 ∨ b = 0 ∨ a < Cardinal.aleph0 ∧ b < Cardinal.aleph0

theorem Cardinal.aleph0_le_mul_iff {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} : Cardinal.aleph0 ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (Cardinal.aleph0 ≤ a ∨ Cardinal.aleph0 ≤ b)

See also Cardinal.aleph0_le_mul_iff.

theorem Cardinal.aleph0_le_mul_iff' {a : Cardinal.{u}} {b : Cardinal.{u}} : Cardinal.aleph0 ≤ a * b ↔ a ≠ 0 ∧ Cardinal.aleph0 ≤ b ∨ Cardinal.aleph0 ≤ a ∧ b ≠ 0

See also Cardinal.aleph0_le_mul_iff'.

theorem Cardinal.mul_lt_aleph0_iff_of_ne_zero {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : a ≠ 0) (hb : b ≠ 0) : a * b < Cardinal.aleph0 ↔ a < Cardinal.aleph0 ∧ b < Cardinal.aleph0

theorem Cardinal.power_lt_aleph0 {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : a < Cardinal.aleph0) (hb : b < Cardinal.aleph0) : a ^ b < Cardinal.aleph0

theorem Cardinal.eq_one_iff_unique {α : Type u_1} : Cardinal.mk α = 1 ↔ Subsingleton α ∧ Nonempty α

theorem Cardinal.infinite_iff {α : Type u} : Infinite α ↔ Cardinal.aleph0 ≤ Cardinal.mk α

theorem Cardinal.aleph0_le_mk_iff {α : Type u} : Cardinal.aleph0 ≤ Cardinal.mk α ↔ Infinite α

theorem Cardinal.mk_lt_aleph0_iff {α : Type u} : Cardinal.mk α < Cardinal.aleph0 ↔ Finite α

@[simp]

theorem Cardinal.aleph0_le_mk (α : Type u) [Infinite α] : Cardinal.aleph0 ≤ Cardinal.mk α

@[simp]

theorem Cardinal.mk_eq_aleph0 (α : Type u_1) [Countable α] [Infinite α] : Cardinal.mk α = Cardinal.aleph0

theorem Cardinal.denumerable_iff {α : Type u} : Nonempty (Denumerable α) ↔ Cardinal.mk α = Cardinal.aleph0

theorem Cardinal.mk_denumerable (α : Type u) [Denumerable α] : Cardinal.mk α = Cardinal.aleph0

theorem Set.countable_infinite_iff_nonempty_denumerable {α : Type u_1} {s : Set α} : s.Countable ∧ s.Infinite ↔ Nonempty (Denumerable ↑s)

@[simp]

theorem Cardinal.aleph0_add_aleph0 : Cardinal.aleph0 + Cardinal.aleph0 = Cardinal.aleph0

theorem Cardinal.aleph0_mul_aleph0 : Cardinal.aleph0 * Cardinal.aleph0 = Cardinal.aleph0

@[simp]

theorem Cardinal.nat_mul_aleph0 {n : ℕ} (hn : n ≠ 0) : ↑n * Cardinal.aleph0 = Cardinal.aleph0

@[simp]

theorem Cardinal.aleph0_mul_nat {n : ℕ} (hn : n ≠ 0) : Cardinal.aleph0 * ↑n = Cardinal.aleph0

@[simp]

theorem Cardinal.ofNat_mul_aleph0 {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n * Cardinal.aleph0 = Cardinal.aleph0

@[simp]

theorem Cardinal.aleph0_mul_ofNat {n : ℕ} [n.AtLeastTwo] : Cardinal.aleph0 * OfNat.ofNat n = Cardinal.aleph0

@[simp]

theorem Cardinal.add_le_aleph0 {c₁ : Cardinal.{u_1}} {c₂ : Cardinal.{u_1}} : c₁ + c₂ ≤ Cardinal.aleph0 ↔ c₁ ≤ Cardinal.aleph0 ∧ c₂ ≤ Cardinal.aleph0

@[simp]

theorem Cardinal.aleph0_add_nat (n : ℕ) : Cardinal.aleph0 + ↑n = Cardinal.aleph0

@[simp]

theorem Cardinal.nat_add_aleph0 (n : ℕ) : ↑n + Cardinal.aleph0 = Cardinal.aleph0

@[simp]

theorem Cardinal.ofNat_add_aleph0 {n : ℕ} [n.AtLeastTwo] : OfNat.ofNat n + Cardinal.aleph0 = Cardinal.aleph0

@[simp]

theorem Cardinal.aleph0_add_ofNat {n : ℕ} [n.AtLeastTwo] : Cardinal.aleph0 + OfNat.ofNat n = Cardinal.aleph0

theorem Cardinal.exists_nat_eq_of_le_nat {c : Cardinal.{u_1}} {n : ℕ} (h : c ≤ ↑n) : ∃ m ≤ n, c = ↑m

theorem Cardinal.mk_int : Cardinal.mk ℤ = Cardinal.aleph0

theorem Cardinal.mk_pNat : Cardinal.mk ℕ+ = Cardinal.aleph0

Cardinalities of basic sets and types

theorem Cardinal.mk_empty : Cardinal.mk Empty = 0

theorem Cardinal.mk_pempty : Cardinal.mk PEmpty.{u_1 + 1} = 0

theorem Cardinal.mk_punit : Cardinal.mk PUnit.{u_1 + 1} = 1

theorem Cardinal.mk_unit : Cardinal.mk Unit = 1

theorem Cardinal.mk_singleton {α : Type u} (x : α) : Cardinal.mk ↑{x} = 1

theorem Cardinal.mk_plift_true : Cardinal.mk (PLift True) = 1

theorem Cardinal.mk_plift_false : Cardinal.mk (PLift False) = 0

@[simp]

theorem Cardinal.mk_vector (α : Type u) (n : ℕ) : Cardinal.mk (Mathlib.Vector α n) = Cardinal.mk α ^ n

theorem Cardinal.mk_list_eq_sum_pow (α : Type u) : Cardinal.mk (List α) = Cardinal.sum fun (n : ℕ) => Cardinal.mk α ^ n

theorem Cardinal.mk_quot_le {α : Type u} {r : α → α → Prop} : Cardinal.mk (Quot r) ≤ Cardinal.mk α

theorem Cardinal.mk_quotient_le {α : Type u} {s : Setoid α} : Cardinal.mk (Quotient s) ≤ Cardinal.mk α

theorem Cardinal.mk_subtype_le_of_subset {α : Type u} {p : α → Prop} {q : α → Prop} (h : ∀ ⦃x : α⦄, p x → q x) : Cardinal.mk (Subtype p) ≤ Cardinal.mk (Subtype q)

theorem Cardinal.mk_emptyCollection (α : Type u) : Cardinal.mk ↑∅ = 0

theorem Cardinal.mk_emptyCollection_iff {α : Type u} {s : Set α} : Cardinal.mk ↑s = 0 ↔ s = ∅

@[simp]

theorem Cardinal.mk_univ {α : Type u} : Cardinal.mk ↑Set.univ = Cardinal.mk α

@[simp]

theorem Cardinal.mk_setProd {α : Type u} {β : Type u} (s : Set α) (t : Set β) : Cardinal.mk ↑(s ×ˢ t) = Cardinal.mk ↑s * Cardinal.mk ↑t

theorem Cardinal.mk_image_le {α : Type u} {β : Type u} {f : α → β} {s : Set α} : Cardinal.mk ↑(f '' s) ≤ Cardinal.mk ↑s

theorem Cardinal.mk_image2_le {α : Type u} {β : Type u} {γ : Type u} {f : α → β → γ} {s : Set α} {t : Set β} : Cardinal.mk ↑(Set.image2 f s t) ≤ Cardinal.mk ↑s * Cardinal.mk ↑t

theorem Cardinal.mk_image_le_lift {α : Type u} {β : Type v} {f : α → β} {s : Set α} : Cardinal.lift.{u, v} (Cardinal.mk ↑(f '' s)) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑s)

theorem Cardinal.mk_range_le {α : Type u} {β : Type u} {f : α → β} : Cardinal.mk ↑(Set.range f) ≤ Cardinal.mk α

theorem Cardinal.mk_range_le_lift {α : Type u} {β : Type v} {f : α → β} : Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) ≤ Cardinal.lift.{v, u} (Cardinal.mk α)

theorem Cardinal.mk_range_eq {α : Type u} {β : Type u} (f : α → β) (h : Function.Injective f) : Cardinal.mk ↑(Set.range f) = Cardinal.mk α

theorem Cardinal.mk_range_eq_lift {α : Type u} {β : Type v} {f : α → β} (hf : Function.Injective f) : Cardinal.lift.{max u w, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{max v w, u} (Cardinal.mk α)

theorem Cardinal.mk_range_eq_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Injective f) : Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{v, u} (Cardinal.mk α)

theorem Cardinal.lift_mk_le_lift_mk_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Injective f) : Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β)

theorem Cardinal.lift_mk_le_lift_mk_of_surjective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Surjective f) : Cardinal.lift.{u, v} (Cardinal.mk β) ≤ Cardinal.lift.{v, u} (Cardinal.mk α)

theorem Cardinal.mk_image_eq_of_injOn {α : Type u} {β : Type u} (f : α → β) (s : Set α) (h : Set.InjOn f s) : Cardinal.mk ↑(f '' s) = Cardinal.mk ↑s

theorem Cardinal.mk_image_eq_of_injOn_lift {α : Type u} {β : Type v} (f : α → β) (s : Set α) (h : Set.InjOn f s) : Cardinal.lift.{u, v} (Cardinal.mk ↑(f '' s)) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)

theorem Cardinal.mk_image_eq {α : Type u} {β : Type u} {f : α → β} {s : Set α} (hf : Function.Injective f) : Cardinal.mk ↑(f '' s) = Cardinal.mk ↑s

theorem Cardinal.mk_image_eq_lift {α : Type u} {β : Type v} (f : α → β) (s : Set α) (h : Function.Injective f) : Cardinal.lift.{u, v} (Cardinal.mk ↑(f '' s)) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)

theorem Cardinal.mk_iUnion_le_sum_mk {α : Type u} {ι : Type u} {f : ι → Set α} : Cardinal.mk ↑(⋃ (i : ι), f i) ≤ Cardinal.sum fun (i : ι) => Cardinal.mk ↑(f i)

theorem Cardinal.mk_iUnion_le_sum_mk_lift {α : Type u} {ι : Type v} {f : ι → Set α} : Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ (i : ι), f i)) ≤ Cardinal.sum fun (i : ι) => Cardinal.mk ↑(f i)

theorem Cardinal.mk_iUnion_eq_sum_mk {α : Type u} {ι : Type u} {f : ι → Set α} (h : Pairwise fun (i j : ι) => Disjoint (f i) (f j)) : Cardinal.mk ↑(⋃ (i : ι), f i) = Cardinal.sum fun (i : ι) => Cardinal.mk ↑(f i)

theorem Cardinal.mk_iUnion_eq_sum_mk_lift {α : Type u} {ι : Type v} {f : ι → Set α} (h : Pairwise fun (i j : ι) => Disjoint (f i) (f j)) : Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ (i : ι), f i)) = Cardinal.sum fun (i : ι) => Cardinal.mk ↑(f i)

theorem Cardinal.mk_iUnion_le {α : Type u} {ι : Type u} (f : ι → Set α) : Cardinal.mk ↑(⋃ (i : ι), f i) ≤ Cardinal.mk ι * ⨆ (i : ι), Cardinal.mk ↑(f i)

theorem Cardinal.mk_iUnion_le_lift {α : Type u} {ι : Type v} (f : ι → Set α) : Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ (i : ι), f i)) ≤ Cardinal.lift.{u, v} (Cardinal.mk ι) * ⨆ (i : ι), Cardinal.lift.{v, u} (Cardinal.mk ↑(f i))

theorem Cardinal.mk_sUnion_le {α : Type u} (A : Set (Set α)) : Cardinal.mk ↑(⋃₀ A) ≤ Cardinal.mk ↑A * ⨆ (s : ↑A), Cardinal.mk ↑↑s

theorem Cardinal.mk_biUnion_le {ι : Type u} {α : Type u} (A : ι → Set α) (s : Set ι) : Cardinal.mk ↑(⋃ x ∈ s, A x) ≤ Cardinal.mk ↑s * ⨆ (x : ↑s), Cardinal.mk ↑(A ↑x)

theorem Cardinal.mk_biUnion_le_lift {α : Type u} {ι : Type v} (A : ι → Set α) (s : Set ι) : Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ x ∈ s, A x)) ≤ Cardinal.lift.{u, v} (Cardinal.mk ↑s) * ⨆ (x : ↑s), Cardinal.lift.{v, u} (Cardinal.mk ↑(A ↑x))

theorem Cardinal.finset_card_lt_aleph0 {α : Type u} (s : Finset α) : Cardinal.mk ↑↑s < Cardinal.aleph0

theorem Cardinal.mk_set_eq_nat_iff_finset {α : Type u_1} {s : Set α} {n : ℕ} : Cardinal.mk ↑s = ↑n ↔ ∃ (t : Finset α), ↑t = s ∧ t.card = n

theorem Cardinal.mk_eq_nat_iff_finset {α : Type u} {n : ℕ} : Cardinal.mk α = ↑n ↔ ∃ (t : Finset α), ↑t = Set.univ ∧ t.card = n

theorem Cardinal.mk_eq_nat_iff_fintype {α : Type u} {n : ℕ} : Cardinal.mk α = ↑n ↔ ∃ (h : Fintype α), Fintype.card α = n

theorem Cardinal.mk_union_add_mk_inter {α : Type u} {S : Set α} {T : Set α} : Cardinal.mk ↑(S ∪ T) + Cardinal.mk ↑(S ∩ T) = Cardinal.mk ↑S + Cardinal.mk ↑T

theorem Cardinal.mk_union_le {α : Type u} (S : Set α) (T : Set α) : Cardinal.mk ↑(S ∪ T) ≤ Cardinal.mk ↑S + Cardinal.mk ↑T

The cardinality of a union is at most the sum of the cardinalities of the two sets.

theorem Cardinal.mk_union_of_disjoint {α : Type u} {S : Set α} {T : Set α} (H : Disjoint S T) : Cardinal.mk ↑(S ∪ T) = Cardinal.mk ↑S + Cardinal.mk ↑T

theorem Cardinal.mk_insert {α : Type u} {s : Set α} {a : α} (h : a ∉ s) : Cardinal.mk ↑(insert a s) = Cardinal.mk ↑s + 1

theorem Cardinal.mk_insert_le {α : Type u} {s : Set α} {a : α} : Cardinal.mk ↑(insert a s) ≤ Cardinal.mk ↑s + 1

theorem Cardinal.mk_sum_compl {α : Type u_1} (s : Set α) : Cardinal.mk ↑s + Cardinal.mk ↑sᶜ = Cardinal.mk α

theorem Cardinal.mk_le_mk_of_subset {α : Type u_1} {s : Set α} {t : Set α} (h : s ⊆ t) : Cardinal.mk ↑s ≤ Cardinal.mk ↑t

theorem Cardinal.mk_le_iff_forall_finset_subset_card_le {α : Type u} {n : ℕ} {t : Set α} : Cardinal.mk ↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n

theorem Cardinal.mk_subtype_mono {α : Type u} {p : α → Prop} {q : α → Prop} (h : ∀ (x : α), p x → q x) : Cardinal.mk { x : α // p x } ≤ Cardinal.mk { x : α // q x }

theorem Cardinal.le_mk_diff_add_mk {α : Type u} (S : Set α) (T : Set α) : Cardinal.mk ↑S ≤ Cardinal.mk ↑(S \ T) + Cardinal.mk ↑T

theorem Cardinal.mk_diff_add_mk {α : Type u} {S : Set α} {T : Set α} (h : T ⊆ S) : Cardinal.mk ↑(S \ T) + Cardinal.mk ↑T = Cardinal.mk ↑S

theorem Cardinal.mk_union_le_aleph0 {α : Type u_1} {P : Set α} {Q : Set α} : Cardinal.mk ↑(P ∪ Q) ≤ Cardinal.aleph0 ↔ Cardinal.mk ↑P ≤ Cardinal.aleph0 ∧ Cardinal.mk ↑Q ≤ Cardinal.aleph0

theorem Cardinal.mk_subtype_of_equiv {α : Type u} {β : Type u} (p : β → Prop) (e : α ≃ β) : Cardinal.mk { a : α // p (e a) } = Cardinal.mk { b : β // p b }

theorem Cardinal.mk_sep {α : Type u} (s : Set α) (t : α → Prop) : Cardinal.mk ↑{x : α | x ∈ s ∧ t x} = Cardinal.mk ↑{x : ↑s | t ↑x}

theorem Cardinal.mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β) (h : Function.Injective f) : Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s)) ≤ Cardinal.lift.{u, v} (Cardinal.mk ↑s)

theorem Cardinal.mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β) (h : s ⊆ Set.range f) : Cardinal.lift.{u, v} (Cardinal.mk ↑s) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s))

theorem Cardinal.mk_preimage_of_injective_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β) (h : Function.Injective f) (h2 : s ⊆ Set.range f) : Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s)) = Cardinal.lift.{u, v} (Cardinal.mk ↑s)

theorem Cardinal.mk_preimage_of_injective_of_subset_range {α : Type u} {β : Type u} (f : α → β) (s : Set β) (h : Function.Injective f) (h2 : s ⊆ Set.range f) : Cardinal.mk ↑(f ⁻¹' s) = Cardinal.mk ↑s

theorem Cardinal.mk_preimage_of_injective {α : Type u} {β : Type u} (f : α → β) (s : Set β) (h : Function.Injective f) : Cardinal.mk ↑(f ⁻¹' s) ≤ Cardinal.mk ↑s

theorem Cardinal.mk_preimage_of_subset_range {α : Type u} {β : Type u} (f : α → β) (s : Set β) (h : s ⊆ Set.range f) : Cardinal.mk ↑s ≤ Cardinal.mk ↑(f ⁻¹' s)

theorem Cardinal.mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α → β) {s : Set α} {t : Set β} (h : t ⊆ f '' s) : Cardinal.lift.{u, v} (Cardinal.mk ↑t) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑{x : α | x ∈ s ∧ f x ∈ t})

theorem Cardinal.mk_subset_ge_of_subset_image {α : Type u} {β : Type u} (f : α → β) {s : Set α} {t : Set β} (h : t ⊆ f '' s) : Cardinal.mk ↑t ≤ Cardinal.mk ↑{x : α | x ∈ s ∧ f x ∈ t}

theorem Cardinal.le_mk_iff_exists_subset {c : Cardinal.{u}} {α : Type u} {s : Set α} : c ≤ Cardinal.mk ↑s ↔ ∃ p ⊆ s, Cardinal.mk ↑p = c

theorem Cardinal.two_le_iff {α : Type u} : 2 ≤ Cardinal.mk α ↔ ∃ (x : α) (y : α), x ≠ y

theorem Cardinal.two_le_iff' {α : Type u} (x : α) : 2 ≤ Cardinal.mk α ↔ ∃ (y : α), y ≠ x

theorem Cardinal.mk_eq_two_iff {α : Type u} : Cardinal.mk α = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ {x, y} = Set.univ

theorem Cardinal.mk_eq_two_iff' {α : Type u} (x : α) : Cardinal.mk α = 2 ↔ ∃! y : α, y ≠ x

theorem Cardinal.exists_not_mem_of_length_lt {α : Type u_1} (l : List α) (h : ↑l.length < Cardinal.mk α) : ∃ (z : α), z ∉ l

theorem Cardinal.three_le {α : Type u_1} (h : 3 ≤ Cardinal.mk α) (x : α) (y : α) : ∃ (z : α), z ≠ x ∧ z ≠ y

powerlt operation

def Cardinal.powerlt (a : Cardinal.{u}) (b : Cardinal.{u}) : Cardinal.{u}

The function a ^< b, defined as the supremum of a ^ c for c < b.

Equations

• a ^< b = ⨆ (c : ↑(Set.Iio b)), a ^ ↑c

def Cardinal.«term_^<_» : Lean.TrailingParserDescr

The function a ^< b, defined as the supremum of a ^ c for c < b.

Equations

• Cardinal.«term_^<_» = Lean.ParserDescr.trailingNode `Cardinal.term_^<_ 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^< ") (Lean.ParserDescr.cat `term 81))

theorem Cardinal.le_powerlt {b : Cardinal.{u}} {c : Cardinal.{u}} (a : Cardinal.{u}) (h : c < b) : a ^ c ≤ a ^< b

theorem Cardinal.powerlt_le {a : Cardinal.{u}} {b : Cardinal.{u}} {c : Cardinal.{u}} : a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c

theorem Cardinal.powerlt_le_powerlt_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (h : b ≤ c) : a ^< b ≤ a ^< c

theorem Cardinal.powerlt_mono_left (a : Cardinal.{u_1}) : Monotone fun (c : Cardinal.{u_1}) => a ^< c

theorem Cardinal.powerlt_succ {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (h : a ≠ 0) : a ^< Order.succ b = a ^ b

theorem Cardinal.powerlt_min {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} : a ^< min b c = min (a ^< b) (a ^< c)

theorem Cardinal.powerlt_max {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} : a ^< max b c = max (a ^< b) (a ^< c)

theorem Cardinal.zero_powerlt {a : Cardinal.{u_1}} (h : a ≠ 0) : 0 ^< a = 1

@[simp]

theorem Cardinal.powerlt_zero {a : Cardinal.{u_1}} : a ^< 0 = 0