isLocalDiffeomorph — Mathlib

English

A C^n diffeomorphism is a local diffeomorphism.

Русский

C^n-диффеоморфизм — это локальный диффеоморфизм.

LaTeX

$$$ IsLocalDiffeomorph I J n Φ \Rightarrow IsLocalDiffeomorphOn I J n Φ $$$

Lean4

/-- A `C^n` diffeomorphism is a local diffeomorphism. -/
theorem isLocalDiffeomorph (Φ : M ≃ₘ^n⟮I, J⟯ N) : IsLocalDiffeomorph I J n Φ := fun _x ↦
  ⟨Φ.toPartialDiffeomorph, by trivial, eqOn_refl Φ _⟩
    -- FUTURE: if useful, also add "a `PartialDiffeomorph` is a local diffeomorphism on its source"

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