mk'_surjective — Mathlib

English

The map mk' f : M × S → M' is surjective; every element of M' can be represented as mk' f m t for some m ∈ M and t ∈ S.

Русский

Карта mk' f: M × S → M' сюръективна; каждый элемент M' можно представить как mk' f m t для некоторых m ∈ M и t ∈ S.

LaTeX

$$$$ \\text{Surj}(mk' f) = \\forall y \\in M', \\exists m \\in M, \\exists s \\in S: mk' f m s = y $$$$

Lean4

theorem mk'_surjective : Function.Surjective (Function.uncurry <| mk' f : M × S → M') :=
  by
  intro x
  obtain ⟨⟨m, s⟩, e : s • x = f m⟩ := IsLocalizedModule.surj S f x
  exact ⟨⟨m, s⟩, mk'_eq_iff.mpr e.symm⟩

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