symm_bijective — Mathlib

English

The map sending an equivalence e to its inverse e^{-1} is a bijection between α ≃ β and β ≃ α.

Русский

Отображение, отправляющее эквивалентность e в её обратную, является биекцией между α ≃ β и β ≃ α.

LaTeX

$$\\text{Bijective}\\left( (e:\\\\alpha \\\\simeq \\\\beta) \\mapsto e^{-1} : \\\\beta \\\\simeq \\\\alpha \\right)$$

Lean4

theorem symm_bijective : Function.Bijective (Equiv.symm : (α ≃ β) → β ≃ α) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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