Theorems · Theorem · functional analysis

TestFunction.continuous_iff_continuous_comp

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} {V : Type u_6} [inst_6 : AddCommGroup V]
  [inst_7 : Module ℝ V] [t : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [LocallyConvexSpace ℝ V]
  [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F] [inst_13 : Module 𝕜 V] [IsScalarTower ℝ 𝕜 V]
  (f : TestFunction Ω F n →ₗ[𝕜] V),
  Continuous ⇑f ↔
    ∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous (⇑f ∘ TestFunction.ofSupportedIn K_sub_Ω)

The universal property of the topology on 𝓓^{n}(Ω, F): a linear map from 𝓓^{n}(Ω, F) to a locally convex topological vector space is continuous if and only if its precomposition with the inclusion ofSupportedIn K_sub_Ω : 𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F) is continuous for every compact K ⊆ Ω.

Defined in

Mathlib.Analysis.Distribution.TestFunction

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedSpaceAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulLocallyConvexSpaceAlgebraIsScalarTowerModuleIsScalarTower