strictAnti_of_lt_sub_one — Mathlib

English

If for all a, ¬IsMin a → f a < f(a−1), then f is strictly anti-monotone.

Русский

Если для всех a, не минимален, f(a) < f(a−1), то f строго антимонотонна.

LaTeX

$$$(\forall a, \neg \mathrm{IsMin}(a) \Rightarrow f(a) < f(a-1)) \Rightarrow \mathrm{StrictAnti}(f)$$$

Lean4

theorem strictAnti_of_lt_sub_one : (∀ a, ¬IsMin a → f a < f (a - 1)) → StrictAnti f := by
  simpa [Order.pred_eq_sub_one] using strictAnti_of_lt_pred (f := f)

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