English
Let s be Ord-connected. If for every a not maximal, with a ∈ s and succ a ∈ s we have f(succ a) ≤ f(a), then f is antitone on s.
Русский
Пусть s является Ord-connected. Если для каждого a, не максимального, при условии a ∈ s и succ(a) ∈ s выполняется f(succ(a)) ≤ f(a), то функция f антимонотонна на s.
LaTeX
$$$\\operatorname{OrdConnected}(s) \\to \\Big( \\forall a\\, (\\neg \\operatorname{IsMax}(a) \\to a \\in s \\to \\operatorname{succ}(a) \\in s \\to f(\\operatorname{succ}(a)) \\le f(a)) \\Big) \\to \\operatorname{AntitoneOn}(f,s).$$$
Lean4
theorem antitoneOn_of_succ_le (hs : s.OrdConnected) (hf : ∀ a, ¬IsMax a → a ∈ s → succ a ∈ s → f (succ a) ≤ f a) :
AntitoneOn f s :=
monotoneOn_of_le_succ (β := βᵒᵈ) hs hf
