surjective_of_isLocalized_span — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem surjective_of_isLocalized_span (H : ∀ r : s, Function.Surjective (map (.powers r.1) (f r) (g r) F)) :
    Function.Surjective F :=
  range_eq_top.mp <|
    eq_top_of_isLocalized₀_span s spn Nₚ g fun r ↦
      (range_localizedMap_eq_localized₀_range _ (f r) (g r) F).symm.trans <| range_eq_top.mpr <| H r

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