continuous_posPart

Mathlib.Analysis.Normed.Order.Lattice

URI: https://scilib.ai/kg/mathlib#continuous_posPart

English

The posPart map x ↦ x⁺ is a continuous function on α.

Русский

Функция положительной части x⁺ непрерывна на α.

LaTeX

$$C( x^{+} )$$

Lean4

@[fun_prop]
theorem continuous_posPart : Continuous (posPart : α → α) :=
  lipschitzWith_posPart.continuous

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

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

Разделы

Аффилиация

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