English
Induction principle for Finsets where f maps elements to a linearly ordered type: if P holds for the empty Finset and whenever a is not in s and f x ≤ f a for all x in s, then P(s) implies P(insert a s), then P holds for all s.
Русский
Индуктивный принцип по максимуму значения: если P пустого множества верно, и если при добавлении элемента a, большего по значению всех x∈s, верно P(s)⇒P(insert a s), то P выполняется для любых s.
LaTeX
$$$ \\forall s\\in \\mathrm{Finset}(\\iota),\\ P(s) \\,\\text{при условии } 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))) $$$
Lean4
/-- Induction principle for `Finset`s in any type from which a given function `f` maps to a linearly
ordered type : a predicate is true on all `s : Finset α` provided that:
* it is true on the empty `Finset`,
* for every `s : Finset α` and an element `a` such that for elements of `s` denoted by `x` we have
`f x ≤ f a`, `p s` implies `p (insert a s)`. -/
@[elab_as_elim]
theorem induction_on_max_value [DecidableEq ι] (f : ι → α) {p : Finset ι → Prop} (s : Finset ι) (h0 : p ∅)
(step : ∀ a s, a ∉ s → (∀ x ∈ s, f x ≤ f a) → p s → p (insert a s)) : p s :=
by
induction s using Finset.eraseInduction with
| _ s ihs
rcases (s.image f).eq_empty_or_nonempty with (hne | hne)
· simp only [image_eq_empty] at hne
simp only [hne, h0]
· have H : (s.image f).max' hne ∈ s.image f := max'_mem (s.image f) hne
simp only [mem_image] at H
rcases H with ⟨a, has, hfa⟩
rw [← insert_erase has]
refine step _ _ (notMem_erase a s) (fun x hx => ?_) (ihs a has)
rw [hfa]
exact le_max' _ _ (mem_image_of_mem _ <| mem_of_mem_erase hx)
