mapₐ_injective_of_injective — Mathlib

English

If f: A → B is injective, then the induced map mapₐ is also injective.

Русский

Если f инъективно отображает A в B, то индукцированное отображение mapₐ тоже инъективно.

LaTeX

$$$\\text{Injective}(f) \\Rightarrow \\text{Injective}(\\text{map}_{A_p,B_p,f})$$$

Lean4

theorem mapₐ_injective_of_injective {f : A →ₐ[R] B} (a : A) [Away a Aₚ] [Away (f a) Bₚ] (hf : Function.Injective f) :
    Function.Injective (mapₐ Aₚ Bₚ f a) :=
  IsLocalization.map_injective_of_injective _ _ _ hf

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