continuous_of_continuous_eval — Mathlib

English

If for every y ∈ E the map a ↦ (g(a))(y) is continuous, then g: α → WeakDual 𝕜 E is continuous.

Русский

Если для каждого y ∈ E отображение a ↦ (g(a))(y) непрерывно, то g: α → WeakDual 𝕜 E непрерывно.

LaTeX

$$$\Big(\forall y \in E,\; a \mapsto (g(a))(y) \text{ is continuous}\Big) \implies g \in C(\alpha, \mathrm{WeakDual}_{\mathbb{k}} E)$$$

Lean4

theorem continuous_of_continuous_eval [TopologicalSpace α] {g : α → WeakDual 𝕜 E}
    (h : ∀ y, Continuous fun a => (g a) y) : Continuous g :=
  continuous_induced_rng.2 (continuous_pi_iff.mpr h)

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