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 strictly antitone on s.
Русский
Пусть s удовлетворяет OrdConnected. Если для каждого 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)) < f(a)) \\Big) \\to \\operatorname{StrictAntiOn}(f,s).$$$
Lean4
theorem strictAntiOn_of_succ_lt (hs : s.OrdConnected) (hf : ∀ a, ¬IsMax a → a ∈ s → succ a ∈ s → f (succ a) < f a) :
StrictAntiOn f s :=
strictMonoOn_of_lt_succ (β := βᵒᵈ) hs hf
