English
For an open partial homeomorphism f: M ⇀ M' between manifolds, differentiability holds on its source and the inverse differentiability holds on its target; i.e., f is MDifferentiable on the source and f^{-1} is MDifferentiable on the target.
Русский
Для открытого частичного гомеоморфа f: M ⇀ M' между мнообразиями дифференцируемость держится на источнике, а дифференцируемость обратной карты — на цели; т.е. f дифференцируема на источнике, а f^{-1} — на цели.
LaTeX
$$$\mathrm{MDifferentiable}_{I,I'}(f) \;\equiv\; \mathrm{MDifferentiableOn}_{I,I'}(f, f_{\mathrm{source}}) \land \mathrm{MDifferentiableOn}_{I',I}(f^{-1}, f_{\mathrm{target}}).$$$
Lean4
/-- Prop registering if an open partial homeomorphism is a local diffeomorphism on its source -/
def MDifferentiable (f : OpenPartialHomeomorph M M') :=
MDifferentiableOn I I' f f.source ∧ MDifferentiableOn I' I f.symm f.target
