isIdealMorphism_of_surjective — Mathlib

English

If f is surjective, then f is an ideal morphism: it sends Lie ideals of L to Lie ideals of L'.

Русский

Если f сюръективен, то он является морфизмом идеалов: отображаетLie-идеалы L в Lie-идеалы L'.

LaTeX

$$$\mathrm{Surjective}(f) \Rightarrow f\,\IsIdealMorphism$$$

Lean4

theorem isIdealMorphism_of_surjective (h : Function.Surjective f) : f.IsIdealMorphism := by
  rw [isIdealMorphism_def, f.idealRange_eq_top_of_surjective h, f.range_eq_top.mpr h, LieIdeal.top_toLieSubalgebra]

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