symm_bijective

Mathlib.Algebra.Order.Hom.Monoid

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

← MathLib Explorer

English

The map that sends an ordered monoid isomorphism to its inverse is bijective.

Русский

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

LaTeX

$$Bijective(symm)$$

Lean4

@[to_additive]
theorem symm_bijective : Function.Bijective (symm : (α ≃*o β) → β ≃*o α) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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