antitone_of_le_pred — Mathlib

English

If for all a not maximal we have f(succ a) ≤ f(a), then Antitone f.

Русский

Если для каждого 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_le_pred (hf : ∀ a, ¬IsMin a → f a ≤ f (pred a)) : Antitone f := by
  simpa using antitoneOn_of_le_pred Set.ordConnected_univ (by simpa using hf)

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