map_neg

Mathlib.LinearAlgebra.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearPMap.map_neg

English

A linear partial map preserves negation: f(-x) = -f(x).

Русский

Линейное частичное отображение сохраняет противоположное: f(-x) = -f(x).

LaTeX

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

Lean4

theorem map_neg (f : E →ₗ.[R] F) (x : f.domain) : f (-x) = -f x :=
  f.toFun.map_neg x

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

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

Разделы

Аффилиация

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