monotone_add_nat_iff_monotoneOn_nat_Ici

English

Monotone of a shifted function is equivalent to monotone on the tail: Monotone (n ↦ f(n+k)) iff MonotoneOn f {x | x ≥ k}.

Русский

Монотонность отображения после сдвига равносильна монотонности на хвосте: Monotone(n ↦ f(n+k)) эквивалентно MonotoneOn f {x | x ≥ k}.

LaTeX

$$$\\mathrm{Monotone}(\\lambda n \\mapsto f(n + k)) \\iff \\mathrm{MonotoneOn} f \\{x \\mid x \\ge k\\}$$$

Lean4

theorem monotone_add_nat_iff_monotoneOn_nat_Ici {f : ℕ → α} {k : ℕ} :
    Monotone (fun n ↦ f (n + k)) ↔ MonotoneOn f {x | k ≤ x} :=
  by
  refine ⟨fun h x hx y hy hle ↦ ?_, fun h x y hle ↦ ?_⟩
  · rw [← Nat.sub_add_cancel hx, ← Nat.sub_add_cancel hy]
    rw [← Nat.sub_le_sub_iff_right hy] at hle
    exact h hle
  · rw [← Nat.add_le_add_iff_right] at hle
    exact h (Nat.le_add_left k x) (Nat.le_add_left k y) hle

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