image_neg_uIcc

Mathlib.Algebra.Order.Group.Pointwise.Interval

URI: https://scilib.ai/kg/mathlib#Set.image_neg_uIcc

English

Negation maps a closed interval [a,b] to the closed interval [−a, −b].

Русский

Отрицание отображает замкнутый интервал [a,b] в замкнутый интервал [−a, −b].

LaTeX

$$$\{ -x \mid x \in [a,b] \} = [-a, -b]$$$

Lean4

theorem image_neg_uIcc : Neg.neg '' [[a, b]] = [[-a, -b]] := by simp

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

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

Разделы

Аффилиация

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