strictAntiOn_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 strictAntiOn_of_lt_pred (hs : s.OrdConnected) (hf : ∀ a, ¬IsMin a → a ∈ s → pred a ∈ s → f a < f (pred a)) :
    StrictAntiOn f s :=
  strictMonoOn_of_pred_lt (β := βᵒᵈ) hs hf

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