bijective_iff_has_inverse — Mathlib

English

Bijective f is equivalent to the existence of a two-sided inverse g with LeftInverse g f and RightInverse g f.

Русский

Биективность f эквивалентна существованию обратной функции g с левым и правым обратными.

LaTeX

$$$ \text{Bijective}(f) \leftrightarrow \exists g, \text{LeftInverse}(g,f) \wedge \text{RightInverse}(g,f) $$$

Lean4

theorem bijective_iff_has_inverse : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f :=
  ⟨fun hf ↦ ⟨_, leftInverse_surjInv hf, rightInverse_surjInv hf.2⟩, fun ⟨_, gl, gr⟩ ↦ ⟨gl.injective, gr.surjective⟩⟩

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