IsLocalDiffeomorph — Mathlib

English

A C^n local diffeomorphism is a map f such that at every x ∈ M there exists a neighborhood where f is a diffeomorphism onto its image, i.e., locally invertible with C^n-inverse.

Русский

Локальный диффеоморфизм класса C^n — это отображение f, для которого в каждой точке x существует окрестность, на которой f является диффеоморфизмом наобраз, то есть локально имеет гладкую обратнообразную карту класса C^n.

LaTeX

$$$ IsLocalDiffeomorph I J n f \iff \forall x:\, M,\; IsLocalDiffeomorphAt I J n f x $$$

Lean4

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

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