approx_le_succ — Mathlib

English

The sequence of approximations is monotone nondecreasing with n: approx n x ≤ approx (n+1) x.

Русский

Последовательность аппроксимаций неубывает: approx n x ≤ approx(n+1) x.

LaTeX

$$$\\forall c\\, \\forall x:\\ approx(n,c,x) \\le approx(n+1,c,x)$$$

Lean4

theorem approx_le_succ (c : CU P) (n : ℕ) (x : X) : c.approx n x ≤ c.approx (n + 1) x := by
  induction n generalizing c with
  | zero =>
    simp only [approx, right_U, right_le_midpoint]
    exact (approx_mem_Icc_right_left c 0 x).2
  | succ n ihn =>
    rw [approx, approx]
    exact midpoint_le_midpoint (ihn _) (ihn _)

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