English
The sets A and B in the right-derivative construction are defined analogously to the left-hand case and satisfy openness/monge properties.
Русский
Множества A и B в конструировании правой производной определяются аналогично левому случаю и удовлетворяют соответствующим свойствам открытости/вложенности.
LaTeX
$$$$A(f,L,r,\varepsilon)\text{ and } B(f,K,r,s,\varepsilon)\text{ defined as above.}$$$$
Lean4
/-- The set `B f K r s ε` is the set of points `x` around which there exists a vector
`L` belonging to `K` (a given set of vectors) such that `h • L` approximates well `f (x + h)`
(up to an error `ε`), simultaneously at scales `r` and `s`. -/
def B (f : ℝ → F) (K : Set F) (r s ε : ℝ) : Set ℝ :=
⋃ L ∈ K, A f L r ε ∩ A f L s ε
