antitone_add_nat_iff_antitoneOn_nat_Ici

English

Antitone of a shifted function is equivalent to tail-antitone: Antitone (λ n, f(n+k)) ↔ AntitoneOn f {x | x ≥ k}.

Русский

Антитонность отображения после сдвига равносильна антитонности на хвосте: Antitone(λ n, f(n+k)) ↔ AntitoneOn f {x | x ≥ k}.

LaTeX

$$$\\mathrm{Antitone}(\\lambda n \\mapsto f(n+k)) \\iff \\mathrm{AntitoneOn} f \\{x \\mid k \\le x\\}$$$

Lean4

theorem antitone_add_nat_iff_antitoneOn_nat_Ici {f : ℕ → α} {k : ℕ} :
    Antitone (fun n ↦ f (n + k)) ↔ AntitoneOn f {x | k ≤ x} :=
  @monotone_add_nat_iff_monotoneOn_nat_Ici αᵒᵈ _ f k

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