cardinalMk_le_max — Mathlib

English

The lifted cardinality of algebraic elements is bounded above by the maximum of the lifted cardinality of R and aleph-null.

Русский

Возвышенная кардинальность алгебраических элементов ограничена максимумом между возведённой кардинальностью R и aleph-null.

LaTeX

$$$\mathrm{lift}\#\{ x \mid IsAlgebraic(R, x) \} \le \max\big( \mathrm{lift}\#R, \aleph_0 \big).$$$

Lean4

@[stacks 09GK]
theorem cardinalMk_le_max : #{ x : A // IsAlgebraic R x } ≤ max #R ℵ₀ :=
  by
  rw [← lift_id #_, ← lift_id #R]
  exact cardinalMk_lift_le_max R A

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