tendsto — Mathlib

English

A map is linear and continuous iff it is bounded.

Русский

Отображение линейно и непрерывно тогда и только тогда, когда оно ограничено.

LaTeX

$$$ \\text{IsLinearMap } 𝕜 f \\wedge \\text{Continuous } f \\iff \\text{IsBoundedLinearMap } 𝕜 f$$$

Lean4

protected theorem tendsto (x : E) (hf : IsBoundedLinearMap 𝕜 f) : Tendsto f (𝓝 x) (𝓝 (f x)) :=
  let ⟨hf, M, _, hM⟩ := hf
  tendsto_iff_norm_sub_tendsto_zero.2 <|
    squeeze_zero (fun _ => norm_nonneg _)
      (fun e =>
        calc
          ‖f e - f x‖ = ‖hf.mk' f (e - x)‖ := by rw [(hf.mk' _).map_sub e x]; rfl
          _ ≤ M * ‖e - x‖ := hM (e - x))
      (suffices Tendsto (fun e : E => M * ‖e - x‖) (𝓝 x) (𝓝 (M * 0)) by simpa
      tendsto_const_nhds.mul (tendsto_norm_sub_self _))

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