inverse_continuousOn — Mathlib

English

If f is approximated linearly on s by a linear surrogate, then the inverse on f(s) is continuous on f(s).

Русский

Если функция f аппроксимируется линейно на s линейным аналогом, то обратная функция на образе f(s) непрерывна на f(s).

LaTeX

$$$\text{ContinuousOn }\left(\left( hf.toPartialEquiv hc \right)^{-1}\right)\left( f( s ) \right)$$$

Lean4

/-- The inverse function is continuous on `f '' s`.
Use properties of `OpenPartialHomeomorph` instead. -/
theorem inverse_continuousOn (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) :
    ContinuousOn (hf.toPartialEquiv hc).symm (f '' s) :=
  by
  apply continuousOn_iff_continuous_restrict.2
  refine ((hf.antilipschitz hc).to_rightInvOn' ?_ (hf.toPartialEquiv hc).right_inv').continuous
  exact fun x hx => (hf.toPartialEquiv hc).map_target hx

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