toWOT_apply

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.toWOT_apply

English

Two objects in E →WOT 𝕜 F are equal iff they agree on all points.

Русский

Два элемента в E →WOT 𝕜 F равны тогда и только тогда, когда они совпадают на всех точках.

LaTeX

$$$A=B \\iff \\forall x, A(x)=B(x)$$$

Lean4

theorem _root_.ContinuousLinearMap.toWOT_apply {A : E →L[𝕜] F} {x : E} :
    ((ContinuousLinearMap.toWOT 𝕜 E F) A) x = A x :=
  rfl

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

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

Разделы

Аффилиация

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