IsLocalDiffeomorphOn — Mathlib

English

The local inverse is itself a local diffeomorphism at f(x).

Русский

Локальная обратная сама является локальной диффеоморфией в точке f(x).

LaTeX

$$$$\\operatorname{IsLocalDiffeomorphAt}\, J\, I\, n\, \\mathrm{localInverse}\; (f\,x).$$$$

Lean4

/-- `f : M → N` is called a **`C^n` local diffeomorphism on *s*** iff it is a local diffeomorphism
at each `x : s`. -/
def IsLocalDiffeomorphOn (f : M → N) (s : Set M) : Prop :=
  ∀ x : s, IsLocalDiffeomorphAt I J n f x

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