coe_inverse'

Mathlib.Algebra.Algebra.NonUnitalHom

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

← MathLib Explorer

English

The underlying function of inverse' equals g.

Русский

Базовая функция inverse' равна g.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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