lift_cardinalMk_le_trdeg — Mathlib

English

If x is algebraically independent over R, then lift #ι ≤ lift(trdeg_R A).

Русский

Пусть x алгебраически независим над R; тогда высота мощности индексации не превосходит подъём трансцендентной степени A над R.

LaTeX

$$$\\text{lift}.{#ι} \\le \\text{lift}.(\\operatorname{trdeg}_R A)$$$

Lean4

theorem lift_cardinalMk_le_trdeg [Nontrivial R] (hx : AlgebraicIndependent R x) : lift.{v} #ι ≤ lift.{u} (trdeg R A) :=
  by
  rw [lift_mk_eq'.mpr ⟨.ofInjective _ hx.injective⟩, lift_le]
  exact le_ciSup_of_le (bddAbove_range _) ⟨_, hx.to_subtype_range⟩ le_rfl

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