symm_bijective — Mathlib

English

The symmetry map that sends an L-equivalence to its inverse, $(M \cong_L N) \to (N \cong_L M)$, is a bijection.

Русский

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

LaTeX

$$$\operatorname{Bijective}\bigl(\operatorname{symm} : (M \cong_L N) \to (N \cong_L M)\bigr)$$$

Lean4

theorem symm_bijective : Function.Bijective (symm : (M ≃[L] N) → _) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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