symm_bijective — Mathlib

English

The map sending a StarAlgEquiv to its inverse is bijective.

Русский

Отображение, отправляющее ⋆-алгебраическое эквивалент на его обратную эквиваленцию, является биекцией.

LaTeX

$$$$ \operatorname{Bijective} \big( \operatorname{symm} : (A \simeq_{\star}^{R} B) \to (B \simeq_{\star}^{R} A) \big). $$$$

Lean4

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

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