to_subtype_range — Mathlib

English

If hx: IsTranscendenceBasis R x, then its range yields IsTranscendenceBasis R ((↑) : range x → A) (with a minor case split when R is subsingleton).

Русский

Если x образует трансцендентальную базу над R, то диапазон x образует трансцендентальную базу над R (с учетом случая, когда R — подмножество одного элемента).

LaTeX

$$$\\mathrm{IsTB}_R(x) \\Rightarrow \\mathrm{IsTB}_R(\\mathrm{Subtype}.val\\vert_{\\mathrm{range} x})$$$

Lean4

theorem to_subtype_range (hx : IsTranscendenceBasis R x) : IsTranscendenceBasis R ((↑) : range x → A) :=
  by
  cases subsingleton_or_nontrivial R
  · rw [isTranscendenceBasis_iff_of_subsingleton] at hx ⊢; infer_instance
  · rwa [isTranscendenceBasis_subtype_range hx.1.injective]

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