English
Let s be Ord-connected. If for all a with not minimal a, a ∈ s and pred a ∈ s, f(pred a) < f a, then StrictMonoOn f s.
Русский
Пусть s ордерно-соединено. Если для любого a с a ∈ s и pred a ∈ s и a не минимален, выполняется f(pred a) < f(a), то StrictMonoOn 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)) < f(a) \\Big) \\to \\operatorname{StrictMonoOn}(f,s).$$$
Lean4
/-- A constructor for `SuccOrder α` for `α` a linear order. -/
@[simps]
def ofCore (succ : α → α) (hn : ∀ {a}, ¬IsMax a → ∀ b, a < b ↔ succ a ≤ b) (hm : ∀ a, IsMax a → succ a = a) :
SuccOrder α :=
{ succ
succ_le_of_lt := fun {a b} => by_cases (fun h hab => (hm a h).symm ▸ hab.le) fun h => (hn h b).mp
le_succ := fun a => by_cases (fun h => (hm a h).symm.le) fun h => le_of_lt <| by simpa using (hn h a).not
max_of_succ_le := fun {a} => not_imp_not.mp fun h => by simpa using (hn h a).not }
