map_surjective — Mathlib

English

If f is a surjective monoid hom, then ConjClasses.map f is surjective on ConjClasses: every conjugacy class in β has a preimage class in α.

Русский

Если f сюръективен как гомоморфизм моноидов, то отображение ConjClasses.map f сюръективно: каждый класс сопряжённости в β имеет прообраз в α.

LaTeX

$$$\text{Surjective}(f) \Rightarrow \text{Surjective}(\mathrm{ConjClasses.map}\, f)$$$

Lean4

theorem map_surjective {f : α →* β} (hf : Function.Surjective f) : Function.Surjective (ConjClasses.map f) :=
  by
  intro b
  obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b
  obtain ⟨a, rfl⟩ := hf b
  exact ⟨ConjClasses.mk a, rfl⟩

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