finset_image_add_of_nonempty — Mathlib

English

Given a nonarchimedean f, a function g: β → α, a Finset t ⊆ β, and t nonempty, there exists b ∈ t such that f(sum over t of g) ≤ f(g(b)).

Русский

Пусть f ненархимедова, g:β→α, и t ⊆ β – непустой конечный сет; существует b ∈ t, такое что f(∑_{i∈t} g(i)) ≤ 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 nonarchimedean function `α → R`, a function `g : β → α` and a nonempty finset
  `t : Finset β`, we can always find `b : β` belonging to `t` such that `f (t.sum g) ≤ f (g b)` . -/
theorem finset_image_add_of_nonempty {α β : Type*} [AddCommMonoid α] [Nonempty β] {f : α → R} (hna : IsNonarchimedean f)
    (g : β → α) {t : Finset β} (ht : t.Nonempty) : ∃ b ∈ t, f (t.sum g) ≤ f (g b) :=
  by
  apply multiset_image_add_of_nonempty hna
  simp_all [Finset.nonempty_iff_ne_empty]

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