isTranscendenceBasis_image — Mathlib

English

For an injective f, IsTranscendenceBasis R (fun x : s => f x) is equivalent to IsTranscendenceBasis R fun x : f''s => (x : A).

Русский

Для инъективного f базис трансцендентности на изображении эквивалентен базису на образе.

LaTeX

$$$\\text{IsTranscendenceBasis } R (\\lambda x:\\, s . f\\, x) \\iff \\text{IsTranscendenceBasis } R (\\lambda x:\\, f''s . x)$$$

Lean4

theorem isTranscendenceBasis_image {ι} {s : Set ι} {f : ι → A} (hf : Set.InjOn f s) :
    IsTranscendenceBasis R (fun x : s ↦ f x) ↔ IsTranscendenceBasis R fun x : f '' s ↦ (x : A) :=
  isTranscendenceBasis_equiv' (Equiv.Set.imageOfInjOn _ _ hf) rfl

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