neg_apply

Mathlib.Topology.ContinuousMap.ZeroAtInfty

URI: https://scilib.ai/kg/mathlib#ZeroAtInftyContinuousMap.neg_apply

English

Negation acts pointwise: for every x, (-f) x = - f x.

Русский

Отрицание действует по точкам: для каждого x выполняется (−f) x = −f(x).

LaTeX

$$(-f)(x) = -f(x).$$

Lean4

theorem neg_apply : (-f) x = -f x :=
  rfl

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

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

Разделы

Аффилиация

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