Theorems · Definition · functional analysis

UniformConvergenceCLM

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

Given E and F two topological vector spaces and 𝔖 : Set (Set E), then UniformConvergenceCLM σ F 𝔖 (denoted E →SLᵤ[σ, 𝔖] F) is a type synonym of E →SL[σ] F equipped with the "topology of uniform convergence on the elements of 𝔖". If the continuous linear image of any element of 𝔖 is bounded, this makes E →SL[σ] F a topological vector space.

Defined in

Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Cited by

44 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedFieldAddCommGroupModuleTopologicalSpaceAddCommGroupModuleTopologicalSpace