English
The lifted cardinality of the set of algebraic elements is bounded above by the product of the lifted cardinality of R[X] and aleph-null.
Русский
Возвышенная кардинальность множества алгебраических элементов ограничена произведением $\mathrm{lift}\#R[X]$ и $\aleph_0$.
LaTeX
$$$\mathrm{lift}\#\{ x \in A \mid IsAlgebraic(R, x) \} \le \mathrm{lift}\#(R[X]) \cdot \aleph_0.$$$
Lean4
theorem cardinalMk_lift_le_mul : Cardinal.lift.{u} #{ x : A // IsAlgebraic R x } ≤ Cardinal.lift.{v} #R[X] * ℵ₀ :=
by
rw [← mk_uLift, ← mk_uLift]
choose g hg₁ hg₂ using fun x : {x : A | IsAlgebraic R x} => x.coe_prop
refine lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le g fun f => ?_
rw [lift_le_aleph0, le_aleph0_iff_set_countable]
suffices MapsTo (↑) (g ⁻¹' { f }) (f.rootSet A) from
this.countable_of_injOn Subtype.coe_injective.injOn (f.rootSet_finite A).countable
rintro x (rfl : g x = f)
exact mem_rootSet.2 ⟨hg₁ x, hg₂ x⟩
