symm_bijective — Mathlib

English

The map sending an isometry equivalence to its inverse is bijective.

Русский

Отображение, отправляющее изометрическую эквивалентность в её обратную, является биекцией.

LaTeX

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

Lean4

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

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