symm_bijective — Mathlib

English

The symmetry operation on open partial homeomorphisms is bijective; it has a two-sided inverse given by itself.

Русский

Операция симметрии над открытыми частичными гомеоморфизмами является биективной; у неё есть двусторонняя обратная функция, равная самой операции.

LaTeX

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

Lean4

theorem symm_bijective :
    Function.Bijective (OpenPartialHomeomorph.symm : OpenPartialHomeomorph X Y → OpenPartialHomeomorph Y X) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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