neg_apply

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

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

English

Negation in the weak operator topology is pointwise: (-f)(x) = -(f(x)).

Русский

Отрицание в слабой операторной топологии по точкам: (-f)(x) = -(f(x)).

LaTeX

$$$(-f)\\,x = -\\bigl(f(x)\\bigr)$$$

Lean4

@[simp]
theorem neg_apply {f : E →WOT[𝕜] F} (x : E) : (-f) x = -(f x) := by simp only [DFunLike.coe]; rfl

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

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

Разделы

Аффилиация

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