Theorems · Theorem · measure theory

MeasureTheory.measurable_image_of_fderivWithin

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E],
  MeasurableSet s → (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → Set.InjOn f s → MeasurableSet (f '' s)

If a function is differentiable and injective on a measurable set, then the image is measurable.

Defined in

Mathlib.MeasureTheory.Function.Jacobian

Cited by

3 results in Mathlib

Foundations

Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpace