isAbsoluteValueNorm — Mathlib

English

The modulus defines an absolute value on the complex numbers: ‖z‖ is nonnegative, zero only at z=0, and satisfies the usual norm properties.

Русский

Модуль задаёт абсолютную величину на множествах комплексных чисел: ‖z‖ неотрицателен, обращается в нуль только при z=0 и удовлетворяет обычным нормированным свойствам.

LaTeX

$$$\|\cdot\| : \mathbb{C} \to \mathbb{R} \text{ is an absolute value on } \mathbb{C}$$$

Lean4

instance isAbsoluteValueNorm : IsAbsoluteValue (‖·‖ : ℂ → ℝ)
    where
  abv_nonneg' := norm_nonneg
  abv_eq_zero' := norm_eq_zero_iff
  abv_add' := norm_add_le
  abv_mul' := Complex.norm_mul

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