IsLocalDiffeomorphAt — Mathlib

English

The image of the local inverse contains the image under f of the base point.

Русский

Образ локального обратного содержит образ точки под действием f.

LaTeX

$$f x ∈ hf.localInverse.source$$

Lean4

/-- `f : M → N` is called a **`C^n` local diffeomorphism at *x*** iff there exist
open sets `U ∋ x` and `V ∋ f x` and a diffeomorphism `Φ : U → V` such that `f = Φ` on `U`. -/
def IsLocalDiffeomorphAt (f : M → N) (x : M) : Prop :=
  ∃ Φ : PartialDiffeomorph I J M N n, x ∈ Φ.source ∧ EqOn f Φ Φ.source

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