symm_bijective — Mathlib

English

The map taking a StarMulEquiv to its inverse is bijective: symm : (A ≃⋆* B) → B ≃⋆* A is bijective.

Русский

Обратное отображение между звездными моноидными эквивалентностями образует биекции: symm : (A ≃⋆* B) → B ≃⋆* A биективно.

LaTeX

$$$\\operatorname{Bijective}(\\mathrm{symm})$$$

Lean4

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

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