English
If f is differentiable at x with derivative f'(x) and some variance condition holds, then x ∈ A(f, f'(x), r, ε) for appropriate r,ε.
Русский
Если f дифференцируема в x с производной f'(x) и выполняются условия, то x ∈ A(f, f'(x), r, ε) для подходящих r,ε.
LaTeX
$$$$\text{If } x \text{ is differentiable at } f, \; f'(x) = L, \; \exists r, ε: x \in A(f,L,r,ε).$$$$
Lean4
/-- Easy inclusion: a differentiability point with derivative in `K` belongs to `D f K`. -/
theorem differentiable_set_subset_D : {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} ⊆ D f K :=
by
intro x hx
rw [D, mem_iInter]
intro e
have : (0 : ℝ) < (1 / 2) ^ e := by positivity
rcases mem_A_of_differentiable this hx.1 with ⟨R, R_pos, hR⟩
obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2) ^ n < R := exists_pow_lt_of_lt_one R_pos (by norm_num : (1 : ℝ) / 2 < 1)
simp only [mem_iUnion, mem_iInter, B, mem_inter_iff]
refine ⟨n, fun p hp q hq => ⟨fderiv 𝕜 f x, hx.2, ⟨?_, ?_⟩⟩⟩ <;>
· refine hR _ ⟨by positivity, lt_of_le_of_lt ?_ hn⟩
exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)
