to_subtype_range' — Mathlib

English

If hx: AlgebraicIndependent R x and ht: range x = t, then AlgebraicIndependent R ((↑) : t → A).

Русский

Если x алгебраически независимо над R и range(x) = t, то элемент t, как подтип, тоже алгебраически независим над R.

LaTeX

$$$\\text{AlgebraicIndependent}_R x \\land \\mathrm{range}(x) = t \\Rightarrow \\text{AlgebraicIndependent}_R(\\mathrm{Subtype}.val|_{t})$$$

Lean4

theorem to_subtype_range' (hx : AlgebraicIndependent R x) {t} (ht : range x = t) :
    AlgebraicIndependent R ((↑) : t → A) :=
  ht ▸ hx.to_subtype_range

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