algebraicIndependent_image — Mathlib

English

If f is injective on a set s, then AlgebraicIndependent R (fun x : s => f x) is equivalent to AlgebraicIndependent R (fun x : f''s => x).

Русский

Если f инъективен на множестве s, то AlgebraicIndependent R (x↦f x) эквивалентно AlgebraicIndependent R (x↦ x) на образе.

LaTeX

$$$\\text{AlgebraicIndependent } R\\, (\\lambda x: f x) \\iff \\text{AlgebraicIndependent } R\\, (\\lambda x: x)$$$

Lean4

theorem algebraicIndependent_image {ι} {s : Set ι} {f : ι → A} (hf : Set.InjOn f s) :
    (AlgebraicIndependent R fun x : s => f x) ↔ AlgebraicIndependent R fun x : f '' s => (x : A) :=
  algebraicIndependent_equiv' (Equiv.Set.imageOfInjOn _ _ hf) rfl

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