mabs

Mathlib.Topology.Algebra.Order.Group

URI: https://scilib.ai/kg/mathlib#ContinuousAt.mabs

English

If f is continuous at x, then |f| is continuous at x.

Русский

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

LaTeX

$$$\mathrm{ContinuousAt}\ f\ x \Rightarrow \mathrm{ContinuousAt}\bigl(\lambda y, |f(y)|\bigr)\ x.$$$

Lean4

@[to_additive (attr := fun_prop)]
protected theorem mabs (h : ContinuousAt f x) : ContinuousAt (fun x => |f x|ₘ) x :=
  Filter.Tendsto.mabs h

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

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

Разделы

Аффилиация

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