seminorm — Mathlib

English

For fixed x ∈ E and y ∈ F*, define the seminorm on E →WOT 𝕜 F by A ↦ ||y(Ax)||; these seminorms generate the weak operator topology.

Русский

Для фиксированных x ∈ E и y ∈ F*, пусть на E →WOT 𝕜 F задана семинормальная функция A ↦ ||y(Ax)||; эти семинормы порождают слабую операторную топологию.

LaTeX

$$def seminorm (x : E) (y : F⋆) : Seminorm 𝕜 (E →WOT[𝕜] F) := toFun A := ||y(Ax)||$$

Lean4

/-- The family of seminorms that induce the weak operator topology, namely `‖y (A x)‖` for
all `x` and `y`. -/
def seminorm (x : E) (y : F⋆) : Seminorm 𝕜 (E →WOT[𝕜] F)
    where
  toFun A := ‖y (A x)‖
  map_zero' := by simp
  add_le' A B := by simpa using norm_add_le _ _
  neg' A := by simp
  smul' r A := by simp

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