English
If K is complete, then every point of D(f,K) is a differentiability point with derivative in K.
Русский
Если K неполно, то каждый x ∈ D(f,K) является точкой правой дифференциации f с производной в K.
LaTeX
$$D f K ⊆ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}$$
Lean4
/-- Easy inclusion: a differentiability point with derivative in `K` belongs to `D f K`. -/
theorem differentiable_set_subset_D :
{x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} ⊆ D f K :=
by
intro x hx
rw [D, mem_iInter]
intro e
have : (0 : ℝ) < (1 / 2) ^ e := pow_pos (by norm_num) _
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 => ⟨derivWithin f (Ici x) x, hx.2, ⟨?_, ?_⟩⟩⟩ <;>
· refine hR _ ⟨pow_pos (by norm_num) _, lt_of_le_of_lt ?_ hn⟩
exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)
