bijective_of_localized_span — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem bijective_of_localized_span (h : ∀ r : s, Function.Bijective (map (.powers r.1) f)) : Function.Bijective f :=
  ⟨injective_of_localized_span _ spn _ fun r ↦ (h r).1, surjective_of_localized_span _ spn _ fun r ↦ (h r).2⟩

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