English
Dual to induction_on_max: induction on min using order duality; a predicate holds for all Finsets if it holds for ∅ and if adding a smaller-than-all-element a preserves the predicate.
Русский
Двойственно induction_on_max: индукция по минимуму через дуальный порядок; предикат выполняется для всех Finset, если он верен для пустого множества и если добавление меньшего элемента сохраняет верность.
LaTeX
$$$\\text{[Induction_on_min]} \\\\forall s:\\ Finset(\\iota) \; (P(\\varnothing) \\\\wedge\\\\ (\\forall a\\, s, a \\notin s \\\\Rightarrow (\\\\forall x\\in s, a < x) \\\\Rightarrow P(s) \\\\Rightarrow P(\\\\mathrm{insert}(a,s)))) \\\\Rightarrow P(s)$$$
Lean4
theorem exists_min_image {α R : Type*} [LinearOrder R] (f : α → R) {s : Multiset α} (hs : s ≠ 0) :
∃ y ∈ s, ∀ z ∈ s, f y ≤ f z :=
@exists_max_image α Rᵒᵈ _ f s hs
