strictAnti_of_succ_lt — Mathlib

English

If for all a not maximal we have f(succ a) < f a, then f is strictly antitone on α.

Русский

Если для каждого a, не максимального, выполняется f(succ(a)) < f(a), то функция f строго антимононтонна на α.

LaTeX

$$$\\Big( \\forall a, \\neg \\operatorname{IsMax}(a) \\to f(\\operatorname{succ}(a)) < f(a) \\Big) \\to \\operatorname{StrictAnti}(f).$$$

Lean4

theorem strictAnti_of_succ_lt (hf : ∀ a, ¬IsMax a → f (succ a) < f a) : StrictAnti f := by
  simpa using strictAntiOn_of_succ_lt Set.ordConnected_univ (by simpa using hf)

Похожие утверждения