abs_eq

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.abs_eq

English

For x ∈ ℝ≥0, |x| = x as a real number.

Русский

Для x ∈ ℝ≥0, |x| = x в действительных числах.

LaTeX

$$$\forall x \in \mathbb{R}_{\ge 0},\ |(x : \mathbb{R})| = x$$$

Lean4

@[simp]
theorem abs_eq (x : ℝ≥0) : |(x : ℝ)| = x :=
  abs_of_nonneg x.property

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

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

Разделы

Аффилиация

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