approx_nonneg — Mathlib

English

For every n and c, and x, the nth approximation is nonnegative.

Русский

Для любого n, c и x аппроксимация неотрицательна.

LaTeX

$$$\\forall c\\,\\forall n\\,\\forall x:\\ 0 \\le a\\n \\text{pp: } approx(n,c,x) \\ge 0$$$

Lean4

theorem approx_nonneg (c : CU P) (n : ℕ) (x : X) : 0 ≤ c.approx n x := by
  induction n generalizing c with
  | zero => exact indicator_nonneg (fun _ _ => zero_le_one) _
  | succ n ihn =>
    simp only [approx, midpoint_eq_smul_add, invOf_eq_inv]
    refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_) <;> apply ihn

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