inv_injective

Mathlib.Data.FunLike.Equiv

URI: https://scilib.ai/kg/mathlib#EquivLike.inv_injective

← MathLib Explorer

English

The inverse operation is injective between equivalent objects.

Русский

Обратная операция инъективна между эквивалентными объектами.

LaTeX

$$$\forall e,g:\, E, \ h:\; e=g \Rightarrow inv(e)=inv(g)\,.$$$

Lean4

theorem inv_injective : Function.Injective (EquivLike.inv : E → β → α) := fun e g h ↦
  coe_injective' e g ((right_inv e).eq_rightInverse (h.symm ▸ left_inv g)) h

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

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

Разделы

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

Аффилиация

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