English
D(f, K) is the set of points where one can approximate f by derivatives in K at smaller and smaller scales; when K is complete, D(f, K) equals the differentiability set with derivative in K.
Русский
D(f, K) — множество точек, в которых f может аппроксимироваться производной в K на все меньших масштабах; при полноте K равняется множеству точек дифференцируемости с производной в K.
LaTeX
$$$$D(f,K) = \bigcap_{e \in \mathbb{N}} \bigcup_{n\in\mathbb{N}} \bigcap_{p\ge n}\bigcap_{q\ge n} B\big(f,K,(1/2)^p,(1/2)^q,(1/2)^e\big).$$$$
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 : E → F) (K : Set (E →L[𝕜] F)) : Set E :=
⋂ e : ℕ, ⋃ n : ℕ, ⋂ (p ≥ n) (q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
