English
The lifted cardinality of L is bounded above by the maximum of the lifted cardinalities of R and ℵ0, via a sigma-polynomial construction.
Русский
Поднятая кардинальность L ограничена максимумом кардинальности R и бесконечного множества ℵ0 через соответствующую конструкцию.
LaTeX
$$$\\text{lift} \\#L \\le \\max \\bigl( \\text{lift} \\#R, \\aleph_0 \\bigr)$$$
Lean4
theorem lift_cardinalMk_le_max : lift.{u} #L ≤ lift.{v} #R ⊔ ℵ₀ :=
calc
lift.{u} #L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) := lift_cardinalMk_le_sigma_polynomial R L
_ = Cardinal.sum fun p : R[X] => #{x : L | x ∈ p.aroots L} := by rw [← mk_sigma]; rfl
_ ≤ Cardinal.sum.{u, v} fun _ : R[X] => ℵ₀ := (sum_le_sum _ _ fun _ => (Multiset.finite_toSet _).lt_aleph0.le)
_ = lift.{v} #(R[X]) * ℵ₀ := by rw [sum_const, lift_aleph0]
_ ≤ lift.{v} (#R ⊔ ℵ₀) ⊔ ℵ₀ ⊔ ℵ₀ :=
((mul_le_max _ _).trans <| by gcongr; simp only [lift_le, Polynomial.cardinalMk_le_max])
_ = _ := by simp
