image_of_comp — Mathlib

English

If s ⊆ ι and g ∘ f has independent values on s, then the image of s under f is independent after applying g.

Русский

Если s ⊆ ι и g ∘ f сохраняет независимость на s, то образ s под действием f сохраняет независимость после применения g.

LaTeX

$$$\text{AlgebraicIndependent}_R\;\text{(g ∘ f) on } s \Rightarrow \text{AlgebraicIndependent}_R\;\text{on } f''s\,.$$

Lean4

theorem image_of_comp {ι ι'} (s : Set ι) (f : ι → ι') (g : ι' → A) (hs : AlgebraicIndependent R fun x : s => g (f x)) :
    AlgebraicIndependent R fun x : f '' s => g x := by
  nontriviality R
  have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp
  exact (algebraicIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs

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