instContinuousLinearMapClass — Mathlib

English

If two weak operator topology maps agree on every argument, they are equal (extensionality principle).

Русский

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

LaTeX

$$$\\forall A,B:\\, (\\forall x:\\, A(x)=B(x)) \\Rightarrow A=B$$$

Lean4

instance instContinuousLinearMapClass : ContinuousLinearMapClass (E →WOT[𝕜] F) 𝕜 E F
    where
  map_add f x y := by simp only [DFunLike.coe]; simp
  map_smulₛₗ f r x := by simp only [DFunLike.coe]; simp
  map_continuous f := ContinuousLinearMap.continuous ((ContinuousLinearMap.toWOT 𝕜 E F).symm f)

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