toFun_eq_coe

Mathlib.Analysis.Normed.Group.Seminorm

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

English

For GroupSeminorm p on E, the function value p.toFun equals p viewed as a function.

Русский

Для GroupSeminorm p на E выполняется, что p.toFun = p как функция.

LaTeX

$$p.toFun = p$$

Lean4

@[to_additive (attr := simp)]
theorem toFun_eq_coe : p.toFun = p :=
  rfl

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

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

Разделы

Аффилиация

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