English
Dual to induction_on_max_value: a predicate holds for all Finsets if it holds for ∅ and if a is not in s with f a ≤ f x for all x ∈ s, then P(insert a s).
Русский
Двойственный к induction_on_max_value; предикат выполняется для всех Finset, если он верен для пустого множества и если при добавлении элемента a меньше любого x ∈ 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(a) \\le f(x)) \\, \\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 a ≤ f x`, `p s` implies `p (insert a s)`. -/
@[elab_as_elim]
theorem induction_on_min_value [DecidableEq ι] (f : ι → α) {p : Finset ι → Prop} (s : Finset ι) (h0 : p ∅)
(step : ∀ a s, a ∉ s → (∀ x ∈ s, f a ≤ f x) → p s → p (insert a s)) : p s :=
@induction_on_max_value αᵒᵈ ι _ _ _ _ s h0 step
