const_abs

Mathlib.Order.Filter.FilterProduct

URI: https://scilib.ai/kg/mathlib#Filter.Germ.const_abs

English

The absolute value commutes with the germ construction: const(abs x) = abs(const x).

Русский

Модуль сохраняется под операцией Герма: const(abs x) = abs(const x).

LaTeX

$$$\\mathrm{const}(\\mathrm{abs} \\, x) = \\mathrm{abs}(\\mathrm{const}\\, x).$$$

Lean4

@[simp]
theorem const_abs [AddCommGroup β] [LinearOrder β] (x : β) : (↑|x| : β*) = |↑x| := by rw [abs_def, map_const]

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

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

Разделы

Аффилиация

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