continuous_dual_apply — Mathlib

English

If for every x and every y in F*, the map a ↦ y(g(a)x) is continuous, then g is continuous.

Русский

Если для каждого x и каждого y в F* отображение a ↦ y(g(a)x) непрерывно, то g непрерывна.

LaTeX

$$$\\forall x\\in E,\\forall y\\in F^*,\\;\\text{Continuous}(a\\mapsto y(g(a)x)) \\Rightarrow \\text{Continuous}(g)$$$

Lean4

theorem continuous_dual_apply (x : E) (y : F⋆) : Continuous fun (A : E →WOT[𝕜] F) => y (A x) := by
  refine (continuous_pi_iff.mp continuous_inducingFn) ⟨x, y⟩

Похожие утверждения