symm_bijective — Mathlib

English

The symmetry map sending an order isomorphism to its inverse is a bijection (and its own inverse up to symm_symm).

Русский

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

LaTeX

$$$ \forall \alpha \beta ([LE \alpha], [LE \beta]), \ \text{Bijective}(\mathrm{OrderIso}.\mathrm{symm})$$$

Lean4

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

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