normAtPlace_add_le — Mathlib

English

normAtPlace w is subadditive: normAtPlace w (x+y) ≤ normAtPlace w x + normAtPlace w y.

Русский

Норма на месте подаддитивна: ||x+y||_w ≤ ||x||_w + ||y||_w.

LaTeX

$$$\operatorname{normAtPlace}(w)(x+y) \leq \operatorname{normAtPlace}(w)(x) + \operatorname{normAtPlace}(w)(y).$$$

Lean4

theorem normAtPlace_add_le (w : InfinitePlace K) (x y : mixedSpace K) :
    normAtPlace w (x + y) ≤ normAtPlace w x + normAtPlace w y :=
  by
  rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
  split_ifs <;> exact norm_add_le _ _

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