countable — Mathlib

English

Under Infinite R, the lifted cardinality 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]
protected theorem countable : Set.Countable {x : A | IsAlgebraic R x} :=
  by
  rw [← le_aleph0_iff_set_countable, ← lift_le_aleph0]
  apply (cardinalMk_lift_le_max R A).trans
  simp

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