Theorems · Theorem · functional analysis

ContinuousMultilinearMap.range_toUniformOnFun

∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : DecidableEq ι]
  [inst_7 : TopologicalSpace F],
  Set.range ContinuousMultilinearMap.toUniformOnFun =
    {f |
      Continuous ((UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f) ∧
        (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
            (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (x + y)) =
              (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x) +
                (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i y)) ∧
          ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
            (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (c • x)) =
              c • (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x)}

Defined in

Mathlib.Topology.Algebra.Module.Multilinear.Topology

Cited by

1 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldTopologicalSpaceAddCommGroupModuleAddCommGroupModuleDecidableEqTopologicalSpace