coe_inverse

Mathlib.Algebra.Algebra.NonUnitalHom

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgHom.coe_inverse

← MathLib Explorer

English

The underlying function of the inverse equals the original inverse function.

Русский

Базовая функция обратного равна заданной обратной функции.

LaTeX

$$$\forall b\in B,\ ((f^{-1} \ g)(b)) = g(b)$$$

Lean4

@[simp]
theorem coe_inverse (f : A →ₙₐ[R] B₁) (g : B₁ → A) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    (inverse f g h₁ h₂ : B₁ → A) = g :=
  rfl

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

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

Разделы

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

Аффилиация

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