Theorems · Definition · functional analysis

PointwiseConvergenceCLM

{𝕜₁ : Type u_4} →
  {𝕜₂ : Type u_5} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (𝕜₁ →+* 𝕜₂) →
          (E : Type u_7) →
            (F : Type u_8) →
              [inst_2 : AddCommGroup E] →
                [TopologicalSpace E] →
                  [inst_4 : AddCommGroup F] → [TopologicalSpace F] → [Module 𝕜₁ E] → [Module 𝕜₂ F] → Type (max u_7 u_8)

The space of continuous linear maps equipped with the topology of pointwise convergence, sometimes also called the strong operator topology. We avoid this terminology since so many other things share similar names, and using "pointwise convergence" in the name is more informative. This topology is also known as the weak⋆-topology in the case that σ = RingHom.id 𝕜 and F = 𝕜

Defined in

Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM

Cited by

21 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Quot.sound

Assumes

NormedFieldNormedFieldAddCommGroupTopologicalSpaceAddCommGroupTopologicalSpaceModuleModule