quotient_norm_add_le — Mathlib

English

The quotient norm satisfies the triangle inequality: ∥x + y∥ ≤ ∥x∥ + ∥y∥ for x, y in the quotient.

Русский

Норма в фактор-группе удовлетворяет неравенству треугольника: ∥x + y∥ ≤ ∥x∥ + ∥y∥.

LaTeX

$$$\|x + y\| \le \|x\| + \|y\|$$$

Lean4

/-- The quotient norm satisfies the triangle inequality. -/
theorem quotient_norm_add_le (S : AddSubgroup M) (x y : M ⧸ S) : ‖x + y‖ ≤ ‖x‖ + ‖y‖ :=
  norm_add_le x y

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