cardinalMk_le_max — Mathlib

English

The lifted cardinality of L is at most the maximum of the lifted cardinality of R and ℵ0, i.e., lift #L ≤ lift #R ⊔ ℵ0.

Русский

Поднятая кардинальность L не больше максимума поднятой кардинальности R и ℵ0.

LaTeX

$$$\\operatorname{lift} \\#L \\le \\operatorname{lift} \\#R \\;\\sqcup\\; \\aleph_0$$

Lean4

/-- The cardinality of an algebraic extension is at most the maximum of the cardinality
of the base ring or `ℵ₀`. -/
@[stacks 09GK]
theorem cardinalMk_le_max : #L ≤ max #R ℵ₀ := by simpa only [lift_id] using lift_cardinalMk_le_max R L

Похожие утверждения