antitone_of_succ_le — Mathlib

English

If for all a with a not maximal we have f(succ a) ≤ f(a), then f is antitone on the whole α.

Русский

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

LaTeX

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

Lean4

theorem antitone_of_succ_le (hf : ∀ a, ¬IsMax a → f (succ a) ≤ f a) : Antitone f := by
  simpa using antitoneOn_of_succ_le Set.ordConnected_univ (by simpa using hf)

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