mabs

Mathlib.Topology.Algebra.Order.Group

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

English

If f is continuous, then the map x ↦ |f(x)| is continuous.

Русский

Если f непрерывна, то отображение x ↦ |f(x)| непрерывно.

LaTeX

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

Lean4

@[to_additive (attr := fun_prop)]
protected theorem mabs (h : Continuous f) : Continuous fun x => |f x|ₘ :=
  continuous_mabs.comp h

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

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

Разделы

Аффилиация

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