coe_zero

Mathlib.Analysis.Normed.Group.Seminorm

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

English

The zero GroupSeminorm corresponds to the constant zero function when viewed as a function.

Русский

Нулевой GroupSeminorm соответствует константной нулевой функции при рассмотрении как функция.

LaTeX

$$⇑(0 : GroupSeminorm E) = 0$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_zero : ⇑(0 : GroupSeminorm E) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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