English
B(f, K, r, s, ε) collects points x for which there exists a linear map L from K that approximates f simultaneously at scales r and s.
Русский
B(f, K, r, s, ε) содержит точки x, для которых существует линейное отображение L из K, аппроксимирующее f одновременно на масштабах r и s.
LaTeX
$$$$B(f,K,r,s,\varepsilon) = \bigcup_{L\in K} A(f,L,r,\varepsilon) \cap A(f,L,s,\varepsilon).$$$$
Lean4
/-- The set `B f K r s ε` is the set of points `x` around which there exists a continuous linear map
`L` belonging to `K` (a given set of continuous linear maps) that approximates well the
function `f` (up to an error `ε`), simultaneously at scales `r` and `s`. -/
def B (f : E → F) (K : Set (E →L[𝕜] F)) (r s ε : ℝ) : Set E :=
⋃ L ∈ K, A f L r ε ∩ A f L s ε
