house_sum_le_sum_house — Mathlib

English

The house is subadditive with respect to addition: the house of a sum is at most the sum of houses.

Русский

Дом удовлетворяет неравенство субаддитивности по сложению: дом суммы не превосходит суммы домов.

LaTeX

$$$\\operatorname{house}\\Big(\\sum_{i\\in s} \\alpha_i\\Big) \\le \\sum_{i\\in s} \\operatorname{house}(\\alpha_i).$$$

Lean4

theorem house_sum_le_sum_house {ι : Type*} (s : Finset ι) (α : ι → K) : house (∑ i ∈ s, α i) ≤ ∑ i ∈ s, house (α i) :=
  by simp only [house, map_sum]; apply norm_sum_le_of_le; intros; rfl

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