ext_dual — Mathlib

English

If two weak operator topology maps agree on all dual evaluations, they are equal.

Русский

Если две слабые операторные топологии отображаются на всех двойственных оценках одинаково, то они равны.

LaTeX

$$$\\forall x\\in E,\\forall y\\in F^*,\\; y(Ax)=y(Bx)\\Rightarrow A=B$$$

Lean4

@[ext 900]
theorem ext_dual [H : SeparatingDual 𝕜 F] {A B : E →WOT[𝕜] F} (h : ∀ x (y : F⋆), y (A x) = y (B x)) : A = B :=
  by
  simp_rw [ext_iff, ← (separatingDual_iff_injective.mp H).eq_iff, LinearMap.ext_iff]
  exact h

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