continuous_clm_apply — Mathlib

English

For finite-dimensional E, continuous CLMs are continuous in the sense that each fixed y yields a continuous function x ↦ f(x) y.

Русский

Для конечномерного E непрерывные линейные отображения – это непрерывно в смысле, что фиксированное y даёт непрерывную функцию x ↦ f(x) y.

LaTeX

$$$[FiniteDimensional 𝕜 E] \\\\Rightarrow (Continuous f) \\\\iff \\\\forall y, Continuous (x \\mapsto f(x) y)$$$

Lean4

theorem continuous_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E] {f : X → E →L[𝕜] F} :
    Continuous f ↔ ∀ y, Continuous (f · y) := by simp_rw [← continuousOn_univ, continuousOn_clm_apply]

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