antitoneOn_of_le_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 AntitoneOn f s.

Русский

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

Lean4

theorem antitoneOn_of_le_pred (hs : s.OrdConnected) (hf : ∀ a, ¬IsMin a → a ∈ s → pred a ∈ s → f a ≤ f (pred a)) :
    AntitoneOn f s :=
  monotoneOn_of_pred_le (β := βᵒᵈ) hs hf

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