inducingFn — Mathlib

English

The inducingFn maps a weak operator topology operator A and a pair (x,y) to y(Ax), bundling as a linear map to show TVS structure.

Русский

Функция inducingFn отправляет слабую операторную топологию A и пару (x,y) в y(Ax), упаковывая как линейное отображение для доказательства структуры TVS.

LaTeX

$$$\\text{inducingFn}: (E \\toWOT[𝕜] F) \\to (E \\times F^* \\to 𝕜)$$$

Lean4

/-- The function that induces the topology on `E →WOT[𝕜] F`, namely the function that takes
an `A` and maps it to `fun ⟨x, y⟩ => y (A x)` in `E × F⋆ → 𝕜`, bundled as a linear map to make
it easier to prove that it is a TVS. -/
def inducingFn : (E →WOT[𝕜] F) →ₗ[𝕜] (E × F⋆ → 𝕜)
    where
  toFun := fun A ⟨x, y⟩ => y (A x)
  map_add' := fun x y => by ext; simp
  map_smul' := fun x y => by ext; simp

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