continuous_of_dual_apply_continuous

English

A higher-level formulation where the same condition yields continuity of g as a map α → E →WOT F.

Русский

Высокоуровневая формулировка, что при том же условии непрерывность импортируется на g: α → E →WOT F.

LaTeX

$$$\\text{Continuous}(a\\mapsto y(g(a)x)) \\Rightarrow \\text{Continuous}(g)$$$

Lean4

@[fun_prop]
theorem continuous_of_dual_apply_continuous {α : Type*} [TopologicalSpace α] {g : α → E →WOT[𝕜] F}
    (h : ∀ x (y : F⋆), Continuous fun a => y (g a x)) : Continuous g :=
  continuous_induced_rng.2 (continuous_pi_iff.mpr fun p => h p.1 p.2)

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