funLike

Mathlib.Algebra.Order.AbsoluteValue.Basic

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.funLike

← MathLib Explorer

English

There is a FunLike structure on AbsoluteValue(R,S).

Русский

Имеется структура FunLike на AbsoluteValue(R,S).

LaTeX

$$$\\\\operatorname{FunLike}(\\\\operatorname{AbsoluteValue}(R,S), R, S)$$$

Lean4

instance funLike : FunLike (AbsoluteValue R S) R S
    where
  coe f := f.toFun
  coe_injective' f g h := by obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := g; congr

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

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

Разделы

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

Аффилиация

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