symm_bijective

Mathlib.Algebra.Order.Hom.Ring

URI: https://scilib.ai/kg/mathlib#OrderRingIso.symm_bijective

English

The symmetry map on OrderRingIso is bijective.

Русский

Обратная карта на OrderRingIso является биективной.

LaTeX

$$$\text{Bijective}(\text{OrderRingIso.symm})$$$

Lean4

theorem symm_bijective : Bijective (OrderRingIso.symm : (α ≃+*o β) → β ≃+*o α) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru