le_of_mem_A — Mathlib

English

If K is complete, then D(f,K) is contained in the differentiability set with derivative in K.

Русский

Если K полно, то D(f,K) ⊆ {x | f differentiable at x and f'(x) ∈ K}.

LaTeX

$$$$D(f,K) \subseteq \{x \mid \text{DifferentiableAt } 𝕜\; f\; x \wedge fderiv 𝕜 f x \in K\}.$$$$

Lean4

theorem le_of_mem_A {r ε : ℝ} {L : E →L[𝕜] F} {x : E} (hx : x ∈ A f L r ε) {y z : E} (hy : y ∈ closedBall x (r / 2))
    (hz : z ∈ closedBall x (r / 2)) : ‖f z - f y - L (z - y)‖ ≤ ε * r :=
  by
  rcases hx with ⟨r', r'mem, hr'⟩
  apply le_of_lt
  exact hr' _ ((mem_closedBall.1 hy).trans_lt r'mem.1) _ ((mem_closedBall.1 hz).trans_lt r'mem.1)

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