strictAnti_of_lt_pred — Mathlib

English

Let s be Ord-connected. If for all a not minimal with a ∈ s and pred a ∈ s we have f(a) < f(pred a), then StrictAntiOn f s.

Русский

Пусть s ордерно-соединено. Если для любого a не минимального с a∈s и pred(a)∈s выполняется f(a) < f(pred a), тогда StrictAntiOn 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(a) < f(\\operatorname{pred}(a)) \\Big) \\to \\operatorname{StrictAntiOn}(f,s).$$$

Lean4

theorem strictAnti_of_lt_pred (hf : ∀ a, ¬IsMin a → f a < f (pred a)) : StrictAnti f := by
  simpa using strictAntiOn_of_lt_pred Set.ordConnected_univ (by simpa using hf)

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