instNormedAddCommGroup

Mathlib.Topology.ContinuousMap.Bounded.Normed

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.instNormedAddCommGroup

← MathLib Explorer

English

The coercion of -f equals the pointwise negation: (−f) = map x ↦ −f(x).

Русский

Коэрцирование −f равно по точкам −f(x).

LaTeX

$$$(-f) = (x \mapsto -f(x))$$$

Lean4

instance instNormedAddCommGroup {α β} [TopologicalSpace α] [NormedAddCommGroup β] : NormedAddCommGroup (α →ᵇ β) :=
  { instSeminormedAddCommGroup with eq_of_dist_eq_zero }

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

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

Разделы

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

Аффилиация

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