cardinalMk_of_infinite — Mathlib

English

If R is infinite, the lifted cardinality of the set of algebraic elements over R in A equals the lifted cardinality of R.

Русский

Если R бесконечно, то возведённая кардинальность алгебраических элементов над R в A равна возведённой кардинальности R.

LaTeX

$$$\mathrm{lift}\#\{ x \in A \mid IsAlgebraic(R, x) \} = \mathrm{lift}\#R.$$$

Lean4

@[simp]
theorem cardinalMk_of_infinite [Infinite R] : #{ x : A // IsAlgebraic R x } = #R :=
  lift_inj.1 <| cardinalMk_lift_of_infinite R A

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