map_le_sum — Mathlib

English

For any finite index set s, if g ≤ v(f(i)) for all i ∈ s, then g ≤ v(∑_{i∈s} f(i)).

Русский

Для любого конечного множества индексов s, если g ≤ v(f(i)) для всех i∈s, тогда g ≤ v(∑_{i∈s} f(i)).

LaTeX

$$$$ \left( \forall i \in s,\ g \le v(f(i)) \right) \Rightarrow g \le v\left(\sum_{i \in s} f(i)\right). $$$$

Lean4

theorem map_le_sum {ι : Type*} {s : Finset ι} {f : ι → R} {g : Γ₀} (hf : ∀ i ∈ s, g ≤ v (f i)) : g ≤ v (∑ i ∈ s, f i) :=
  v.map_sum_le hf

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