lim_zero_bounded_linear_map — Mathlib

English

Let f: E → F be a bounded linear map between normed spaces. Then f(x) tends to 0 as x tends to 0; equivalently, Tendsto f (𝓝 0) (𝓝 0).

Русский

Пусть f: E → F является ограниченным линейным отображением между нормально нормированными пространствами. Тогда f(x) стремится к 0 при x → 0; эквивалентно Tendsto f (𝓝 0) (𝓝 0).

LaTeX

$$$IsBoundedLinearMap\ 𝕜\ f\rightarrow \operatorname{Tendsto} f (\mathcal{N}(0)) (\mathcal{N}(0))$$$

Lean4

theorem lim_zero_bounded_linear_map (hf : IsBoundedLinearMap 𝕜 f) : Tendsto f (𝓝 0) (𝓝 0) :=
  (hf.1.mk' _).map_zero ▸ continuous_iff_continuousAt.1 hf.continuous 0

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