symm_bijective — Mathlib

English

The symmetry operator on PEquiv is bijective: PEquiv.symm is a bijection between PEquiv α β and PEquiv β α.

Русский

Операция симметрии на PEquiv обратно-функции является биекция: PEquiv.symm устанавливает биективное соответствие между PEquiv α β и PEquiv β α.

LaTeX

$$$$ \\mathrm{Bijective}(\\mathrm{PEquiv.symm}). $$$$

Lean4

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

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