measurable_image_of_fderivWithin — Mathlib

English

One can partition the domain into countably many disjoint measurable pieces where f is well approximated by linear maps.

Русский

Можно разбить область на счетное число непересекающихся измеримых частей, где f хорошо приближена линейными картами.

LaTeX

$$$$ \exists t_n, A_n : \ \\text{PairwiseDisjoint on } t, \ f\text{ approximated by } A_n \text{ on } s \cap t_n $$$$

Lean4

/-- If a function is differentiable and injective on a measurable set,
then the image is measurable. -/
theorem measurable_image_of_fderivWithin (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
    (hf : InjOn f s) : MeasurableSet (f '' s) :=
  haveI : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt
  hs.image_of_continuousOn_injOn (DifferentiableOn.continuousOn this) hf

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