map_lt_sum — Mathlib

English

If g ≠ ⊤ and g < v(f(i)) for all i ∈ s, then g < v(∑_{i∈s} f(i)).

Русский

Если g ≠ ⊤ и g < v(f(i)) для всех i ∈ s, то g < v(∑_{i∈s} f(i)).

LaTeX

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

Lean4

theorem map_lt_sum {ι : Type*} {s : Finset ι} {f : ι → R} {g : Γ₀} (hg : g ≠ ⊤) (hf : ∀ i ∈ s, g < v (f i)) :
    g < v (∑ i ∈ s, f i) :=
  v.map_sum_lt hg hf

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