English
Let F be a normed additive commutative group and f: R → F. For any K ⊆ F, the set D(f,K) (defined by a countable intersection/union construction) coincides with the set of all points x ∈ R at which f is differentiable from the right with derivative in K, provided K is complete.
Русский
Пусть F — нормированная арабова группа, f: R → F. Для любого подмножества K ⊆ F множество D(f,K) (задаётся как счетное пересечение и объединение) совпадает с множеством всех точек x ∈ R, в которых f дифференцируема справа и производная принадлежит K, при условии, что K полное.
LaTeX
$$$D f K = \\{ x \\in \\mathbb{R} \\mid \\text{DifferentiableWithinAt } \\mathbb{R} f (I_c i x) x \\land \\ derivWithin f (Ici x) x \\in K \\}, \\quad \\text{если } K \\text{ полно}.$$$
Lean4
/-- The set `D f K` is a complicated set constructed using countable intersections and unions. Its
main use is that, when `K` is complete, it is exactly the set of points where `f` is differentiable,
with a derivative in `K`. -/
def D (f : ℝ → F) (K : Set F) : Set ℝ :=
⋂ e : ℕ, ⋃ n : ℕ, ⋂ (p ≥ n) (q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
