isAbsoluteValue_norm — Mathlib

English

The real-valued norm on a normed ring satisfies the axioms of an absolute value: nonnegativity, zero only at 0, triangle inequality, and multiplicativity.

Русский

Действительная норма на нормированном кольце удовлетворяет аксиомам модуля: неотрицательность, нуль только при 0, треугольное неравенство и мультипликативность.

LaTeX

$$$\\text{IsAbsoluteValue}(\\|\\cdot\\|)\\,. (\\text{norm})$$$

Lean4

instance isAbsoluteValue_norm : IsAbsoluteValue (norm : α → ℝ)
    where
  abv_nonneg' := norm_nonneg
  abv_eq_zero' := norm_eq_zero
  abv_add' := norm_add_le
  abv_mul' := norm_mul

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