continuous_of_continuous_eval — Mathlib

English

If B is injective as a map E → F → 𝕜, then the coercion x ↦ (y ↦ B(x,y)) is an embedding.

Русский

Если отображение B инъективно, то отображение x ↦ (y ↦ B(x,y)) единообразно встраивает E в пространство функций.

LaTeX

$$IsEmbedding (fun (x : WeakBilin B) y => B x y) under injectivity of B$$

Lean4

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

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