continuous_of_locally_bounded — Mathlib

English

If a locally bounded semilinear map f: E →ₛₗ[σ] F has the stated boundedness property on von Neumann bounded sets, then f is globally continuous.

Русский

Если локально ограниченное полилинейное отображение f: E →ₛₗ[σ] F обладает указанным свойством ограниченности на множества фон Неймена, то оно непрерывно на всей области определения.

LaTeX

$$$\forall s,\ IsVonNBounded_{\mathbb{k}}(s) \Rightarrow IsVonNBounded_{\mathbb{k}'}(f''s) \Rightarrow Continuous(f)$$$

Lean4

/-- If `E` is first countable, then every locally bounded linear map `E →ₛₗ[σ] F` is continuous. -/
theorem continuous_of_locally_bounded [IsUniformAddGroup F] (f : E →ₛₗ[σ] F)
    (hf : ∀ s, IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (f '' s)) : Continuous f :=
  (uniformContinuous_of_continuousAt_zero f <| f.continuousAt_zero_of_locally_bounded hf).continuous

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