symm_bijective — Mathlib

English

The map that sends a partial equivalence to its inverse is bijective; in fact it is an involution since symm(symm(e)) = e.

Русский

Переход от частичного эквив к его обратному отображению является биекцией; по сути это инволюция, так как symm(symm(e)) = e.

LaTeX

$$Function.Bijective(PartialEquiv.symm)$$

Lean4

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

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