abs_def

Mathlib.Order.Filter.FilterProduct

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

English

For x ∈ β*, |x| equals map abs x, i.e., the absolute value is preserved under Germ construction.

Русский

Для x ∈ β*, равенство |x| сохраняется в Germ: |x| = map abs x.

LaTeX

$$$|x| = \\mathrm{map}\\ \\mathrm{abs}\\ x.$$$

Lean4

theorem abs_def [AddCommGroup β] [LinearOrder β] (x : β*) : |x| = map abs x :=
  inductionOn x fun _a => rfl

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

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

Разделы

Аффилиация

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