English
Induction principle for Finsets of type β mapping to a linearly ordered α: with a predicate P on Finset ι, if P holds for empty and if adding a not-in-s element a with f(x) ≤ f(a) for all x ∈ s preserves P, then P holds for all s.
Русский
Индуктивный принцип на максимум значения (вариант): для Finset ι в линейно упорядоченном α с отображением f, если P(пустое) и добавление элемента a с f(x) ≤ f(a) сохраняет P, то P выполняется для всех s.
LaTeX
$$$ \\forall s:\\ Finset(\\iota),\\ P(\\varnothing) \\\\wedge\\\\ (\\forall a\\,s, a \\notin s \\Rightarrow (\\forall x\\in s, f(x) \\le f(a)) \\Rightarrow P(s) \\Rightarrow P(\\mathrm{insert}(a,s))) \\\\Rightarrow P(s)$$$
Lean4
theorem exists_max_image {α R : Type*} [LinearOrder R] (f : α → R) {s : Multiset α} (hs : s ≠ 0) :
∃ y ∈ s, ∀ z ∈ s, f z ≤ f y := by
classical
obtain ⟨y, hys, hy⟩ := Finset.exists_max_image s.toFinset f (toFinset_nonempty.mpr hs)
exact ⟨y, mem_toFinset.mp hys, fun _ hz ↦ hy _ (mem_toFinset.mpr hz)⟩
