eq_comp_symm

Mathlib.Algebra.Order.Hom.Monoid

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

English

The inverse map symm is a bijection, with inverse given by symm itself.

Русский

Обратная карта symm — биекция, у которой обратное отображение снова symm.

LaTeX

$$Bijective(\\n symm)$$

Lean4

@[to_additive]
theorem eq_comp_symm (e : α ≃*o β) (f : β → α) (g : α → α) : f = g ∘ e.symm ↔ f ∘ e = g :=
  e.toEquiv.eq_comp_symm f g

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

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

Разделы

Аффилиация

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