symm_bijective — Mathlib

English

The map sending an isomorphism to its symmetric is bijective (i.e., has a two-sided inverse).

Русский

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

LaTeX

$$$\\forall {C} [\\mathrm{Category}(C)], \\ \\mathrm{Function.Bijective}(\\mathrm{symm})$$$

Lean4

theorem symm_bijective {X Y : C} : Function.Bijective (symm : (X ≅ Y) → _) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm_eq, symm_symm_eq⟩

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