measurableEmbedding_of_fderivWithin

English

If f is differentiable on a measurable set and injective, then the restriction provides a measurable embedding.

Русский

Если f дифференцируема на измеримом множестве и инъективна, то ограничение задаёт измеримое вложение.

LaTeX

$$$$ \text{MeasurableEmbedding }(s\restriction f) $$$$

Lean4

/-- If a function is differentiable and injective on a measurable set `s`, then its restriction
to `s` is a measurable embedding. -/
theorem measurableEmbedding_of_fderivWithin (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
    (hf : InjOn f s) : MeasurableEmbedding (s.restrict f) :=
  haveI : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt
  this.continuousOn.measurableEmbedding hs hf

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