Theorems · Definition · functional analysis

CompactConvergenceCLM

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

The topology of compact convergence on E →L[𝕜] F.

Defined in

Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM

Cited by

14 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedFieldAddCommGroupModuleAddCommGroupModuleTopologicalSpaceTopologicalSpace