English
Let s be Ord-connected. If for all a not minimal with a ∈ s and pred a ∈ s we have f(pred a) ≤ f a, then f is monotone on s.
Русский
Пусть s двойственно ордерно-соединённо. Если для каждого a, не минимального, с a ∈ s и pred a ∈ s выполняется f(pred a) ≤ f(a), то f монотонна на s.
LaTeX
$$$\\operatorname{OrdConnected}(s) \\to \\Big( \\forall a, \\neg \\operatorname{IsMin}(a) \\to a \\in s \\to \\operatorname{pred}(a) \\in s \\to f(\\operatorname{pred}(a)) \\le f(a) \\Big) \\to \\operatorname{MonotoneOn}(f,s).$$$
Lean4
theorem monotoneOn_of_pred_le (hs : s.OrdConnected) (hf : ∀ a, ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a) :
MonotoneOn f s := by
rintro a ha b hb hab
obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab
clear hab
induction n with
| zero => simp
| succ n hn =>
rw [Function.iterate_succ_apply'] at ha ⊢
have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
by_cases ha' : IsMin (pred^[n] b)
· rw [pred_eq_iff_isMin.2 ha']
exact hn this
· exact (hn this).trans' (hf _ ha' this ha)
