norm'

Mathlib.Analysis.Normed.Group.Continuity

URI: https://scilib.ai/kg/mathlib#Filter.Tendsto.norm'

English

If f is a function, then the map x ↦ ‖f x‖ is continuous at a whenever f is continuous at a.

Русский

Если f непрерывна в точке a, то x ↦ ‖f x‖ непрерывна в a.

LaTeX

$$$ \text{ContinuousAt}(f,a) \Rightarrow \text{ContinuousAt}(\lambda x.\|f x\|, a). $$$

Lean4

@[to_additive Filter.Tendsto.norm]
theorem norm' (h : Tendsto f l (𝓝 a)) : Tendsto (fun x => ‖f x‖) l (𝓝 ‖a‖) :=
  tendsto_norm'.comp h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru