rightHom_surjective — Mathlib

English

Let N, G be groups and φ : G →* MulAut N. The projection rightHom: N ⋊[φ] G → G is surjective; equivalently, for every g ∈ G there exists x ∈ N ⋊[φ] G with rightHom(x) = g.

Русский

Пусть N и G — группы, φ: G →* MulAut N. Проецирование rightHom: N ⋊[φ] G → G сюръективно; то есть для любого g ∈ G существует x ∈ N ⋊[φ] G такое, что rightHom(x) = g.

LaTeX

$$$\forall g \in G, \exists x \in N \rtimes_{\varphi} G:\ rightHom(x) = g.$$$

Lean4

theorem rightHom_surjective : Function.Surjective (rightHom : N ⋊[φ] G → G) :=
  Function.surjective_iff_hasRightInverse.2 ⟨inr, rightHom_inr⟩

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