English
For a nonarchimedean f, a function g: β → α, and a nonempty Finset t, there exists b ∈ t with f(sum g t) ≤ f(g b).
Русский
Для ненархимедовой f, отображения g и непустого Finset t существует b ∈ t такое, что f(сумма g над t) ≤ f(g(b)).
LaTeX
$$$\\exists b \\in t\\;\\text{ such that }\\ f\\Big(\\sum_{i\\in t} g(i)\\Big) \\le f(g(b))$$$
Lean4
/-- Given a nonnegative nonarchimedean function `α → R` such that `f 0 = 0`, a function `g : β → α`
and a finset `t : Finset β`, we can always find `b : β`, belonging to `t` if `t` is nonempty,
such that `f (t.sum g) ≤ f (g b)` . -/
theorem finset_image_add {F α β : Type*} [AddCommMonoid α] [FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R]
[Nonempty β] {f : F} (hna : IsNonarchimedean f) (g : β → α) (t : Finset β) :
∃ b : β, (t.Nonempty → b ∈ t) ∧ f (t.sum g) ≤ f (g b) :=
by
have h1 : t.Nonempty ↔ t.val ≠ 0 := by simp [Finset.nonempty_iff_ne_empty]
rw [h1]
exact multiset_image_add hna g t.val
