toFun_eq_coe

Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

URI: https://scilib.ai/kg/mathlib#AlgebraNorm.toFun_eq_coe

English

An algebra norm p coincides with its canonical real-valued function; i.e., p.toFun = p as a real-valued function.

Русский

Алгебраическая норма p совпадает с своей канонической функцией в вещественном значении; то есть p.toFun = p как вещественная функция.

LaTeX

$$$p.toFun = p$$$

Lean4

theorem toFun_eq_coe (p : AlgebraNorm R S) : p.toFun = p :=
  rfl

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

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

Разделы

Аффилиация

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