inv_surjective — Mathlib

English

The inversion map on a group with involutive inverse is surjective; every element has a preimage under inversion.

Русский

Обратное отображение в группе с инволютивным оборотом сюрьективно; каждому элементу сопоставим обратное.

LaTeX

$$$\forall y \in G,\ \exists x \in G,\ x^{-1} = y$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_surjective : Function.Surjective (Inv.inv : G → G) :=
  inv_involutive.surjective

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