continuous_negPart

Mathlib.Analysis.Normed.Order.Lattice

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

English

The negPart map x ↦ x⁻ is a continuous function on α.

Русский

Отрицательная часть x⁻ непрерывна на α.

LaTeX

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

Lean4

@[fun_prop]
theorem continuous_negPart : Continuous (negPart : α → α) :=
  lipschitzWith_negPart.continuous

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

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

Разделы

Аффилиация

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