injective_of_isLocalized_span — Mathlib

English

If for every r in s, the map in the localized setting is injective, then the global map is injective.

Русский

Если для каждого r ∈ s отображение в локализованной обстановке инъективно, то глобальное отображение инъективно.

LaTeX

$$$\\forall r\\in s,\\; \\text{Injective}(\\text{map}(.powers r.1)(f)) \\Rightarrow \\text{Injective}(f)$$$

Lean4

theorem injective_of_isLocalized_span (H : ∀ r : s, Function.Injective (map (.powers r.1) (f r) (g r) F)) :
    Function.Injective F := fun x y eq ↦ Module.eq_of_isLocalized_span _ spn _ f _ _ fun P ↦ H P <| by simp [eq]

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