le_of_mem_A — Mathlib

English

If x ∈ A(f,L,r,ε) and y,z lie in the interval [x, x + r/2], then a certain linear bound involving L and ε holds on f(z) - f(y).

Русский

Если x ∈ A(f,L,r,ε) и y,z лежат в [x, x + r/2], то имеет место неравенство на величину \\|f(z) - f(y) - (z - y) L\\|.

LaTeX

$$\\|f z - f y - (z - y) • L\\| ≤ ε * r$$

Lean4

theorem le_of_mem_A {r ε : ℝ} {L : F} {x : ℝ} (hx : x ∈ A f L r ε) {y z : ℝ} (hy : y ∈ Icc x (x + r / 2))
    (hz : z ∈ Icc x (x + r / 2)) : ‖f z - f y - (z - y) • L‖ ≤ ε * r :=
  by
  rcases hx with ⟨r', r'mem, hr'⟩
  have A : x + r / 2 ≤ x + r' := by linarith [r'mem.1]
  exact hr' _ ((Icc_subset_Icc le_rfl A) hy) _ ((Icc_subset_Icc le_rfl A) hz)

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