symm_bijective — Mathlib

English

The map sending a continuous algebraic equivalence to its symmetry is bijective.

Русский

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

LaTeX

$$$\text{Bijective}(\mathrm{ContinuousAlgEquiv}.\mathrm{symm})$$$

Lean4

theorem symm_bijective : Function.Bijective (symm : (A ≃A[R] B) → _) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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