cardinalMk_lift_of_infinite — Mathlib

English

If R is infinite, then 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_lift_of_infinite [Infinite R] :
    Cardinal.lift.{u} #{ x : A // IsAlgebraic R x } = Cardinal.lift.{v} #R :=
  ((cardinalMk_lift_le_max R A).trans_eq (max_eq_left <| aleph0_le_mk _)).antisymm <|
    lift_mk_le'.2
      ⟨⟨fun x => ⟨algebraMap R A x, isAlgebraic_algebraMap _⟩, fun _ _ h =>
          FaithfulSMul.algebraMap_injective R A (Subtype.ext_iff.1 h)⟩⟩

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