ext_iff

Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

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

English

Equivalence of ext_iff holds: A=B iff ∀ x, A x = B x.

Русский

Эквивалентность ext_iff: A=B iff ∀ x, A x = B x.

LaTeX

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

Lean4

theorem ext_iff {A B : E →WOT[𝕜] F} : A = B ↔ ∀ x, A x = B x :=
  ContinuousLinearMap.ext_iff

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

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

Разделы

Аффилиация

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