lift_surjective_of_surjective — Mathlib

English

If φ is surjective and N ≤ ker φ, then the descended map G/N → M is surjective.

Русский

Если φ сюръективна и N ≤ ker φ, то спусковое отображение G/N → M сюръективно.

LaTeX

$$$N \\le \\ker \\varphi \\;\\Longrightarrow\\; \\mathrm{lift}\\;N\\;\\varphi\\;HN:\\; G/N \\twoheadrightarrow M.$$$

Lean4

@[to_additive]
theorem lift_surjective_of_surjective (φ : G →* M) (hφ : Function.Surjective φ) (HN : N ≤ φ.ker) :
    Function.Surjective (QuotientGroup.lift N φ HN) :=
  Quotient.lift_surjective _ _ hφ

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