contMDiffOn — Mathlib

English

A C^n local diffeomorphism on s is equivalent to being a local diffeomorphism at every point of s.

Русский

Локальный диффеоморфизм класса C^n на области s эквивалентен тому, что в каждой точке этой области он локальный диффеоморфизм.

LaTeX

$$$ IsLocalDiffeomorphOn I J n f s \iff \forall x:\, x\in s, IsLocalDiffeomorphAt I J n f x $$$

Lean4

/-- A `C^n` local diffeomorphism on `s` is `C^n` on `s`. -/
theorem contMDiffOn (hf : IsLocalDiffeomorphOn I J n f s) : ContMDiffOn I J n f s := fun x hx ↦
  (hf ⟨x, hx⟩).contMDiffAt.contMDiffWithinAt

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