A — Mathlib · SciLib

English

In the complete case, D f K equals the differentiability set with derivative in K.

Русский

В случае полноты D f K равняется множеству точек дифференцируемости с производной в K.

LaTeX

$$$$D(f,K) = \{x \mid \text{DifferentiableAt } 𝕜\; f\; x \wedge fderiv 𝕜 f x \in K\}.$$$$

Lean4

/-- The set `A f L r ε` is the set of points `x` around which the function `f` is well approximated
at scale `r` by the linear map `h ↦ h • L`, up to an error `ε`. We tweak the definition to
make sure that this is open on the right. -/
def A (f : ℝ → F) (L : F) (r ε : ℝ) : Set ℝ :=
  {x | ∃ r' ∈ Ioc (r / 2) r, ∀ᵉ (y ∈ Icc x (x + r')) (z ∈ Icc x (x + r')), ‖f z - f y - (z - y) • L‖ ≤ ε * r}

Похожие утверждения