continuous_of_linear_of_bound — Mathlib

English

If a linear map f: E → G is additive, homogeneous, and bounded by a real C, then f is continuous.

Русский

Если линейная карта непрерывна и ограничена константой C, то она непрерывна.

LaTeX

$$$\exists C\in\mathbb{R},\forall x\in E:\|f x\|\le C\|x\| \Rightarrow \text{Continuous}(f)$$$

Lean4

theorem continuous_of_linear_of_bound {f : E → G} (h_add : ∀ x y, f (x + y) = f x + f y)
    (h_smul : ∀ (c : 𝕜) (x), f (c • x) = c • f x) {C : ℝ} (h_bound : ∀ x, ‖f x‖ ≤ C * ‖x‖) : Continuous f :=
  let φ : E →ₗ[𝕜] G :=
    { toFun := f
      map_add' := h_add
      map_smul' := h_smul }
  AddMonoidHomClass.continuous_of_bound φ C h_bound

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