sequence_anti — Mathlib

English

Let f: α → β with β a preorder and hf: Directed (≥) f. Then the sequence i ↦ f(hf.sequence f i) is antitone, i.e. as i increases, the f-values do not increase.

Русский

Пусть f: α → β, где β образовано с предикатом порядка, и hf: Directed (≥) f. Тогда последовательность i ↦ f(hf.sequence f i) является антимонотной: при увеличении i значения f не возрастает.

LaTeX

$$$ \\forall i\\le j:\\; f\\big(hf.sequence\\,f(i)\\big) \\ge f\\big(hf.sequence\\,f(j)\\big).$$$

Lean4

theorem sequence_anti : Antitone (f ∘ hf.sequence f) :=
  antitone_nat_of_succ_le <| hf.sequence_mono_nat

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