injective_of_localized_span — Mathlib

English

If every localized map is injective, then the whole localization setup yields injectivity.

Русский

Если каждая локализованная карта инъективна, то локализованная конфигурация обеспечивает инъективность.

LaTeX

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

Lean4

theorem injective_of_localized_span (h : ∀ r : s, Function.Injective (map (.powers r.1) f)) : Function.Injective f :=
  injective_of_isLocalized_span s spn _ (fun _ ↦ mkLinearMap _ _) _ (fun _ ↦ mkLinearMap _ _) f h

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