inducingFn_apply

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

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

English

Applying inducingFn to a pair (x,y) yields y(Ax).

Русский

Применение inducingFn к пару (x,y) даёт y(Ax).

LaTeX

$$$\\text{inducingFn}(\\,A\\,)(\\langle x,y\\rangle) = y(Ax)$$$

Lean4

@[simp]
theorem inducingFn_apply {f : E →WOT[𝕜] F} {x : E} {y : F⋆} : inducingFn 𝕜 E F f (x, y) = y (f x) :=
  rfl

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

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

Разделы

Аффилиация

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