mdifferentiableAt — Mathlib

English

The source of the local inverse is open in the topology.

Русский

Область определения локального обратного открыта в топологии.

LaTeX

$$IsOpen hf.localInverse.source$$

Lean4

protected theorem mdifferentiableAt (hn : 1 ≤ n) {x : M} (hx : x ∈ Φ.source) : MDifferentiableAt I J Φ x :=
  (Φ.mdifferentiableOn hn x hx).mdifferentiableAt
    (Φ.open_source.mem_nhds hx)
      /- We could add lots of additional API (following `Diffeomorph` and `OpenPartialHomeomorph`),
      such as
      * further continuity and differentiability lemmas
      * refl and trans instances; lemmas between them.
      As this declaration is meant for internal use only, we keep it simple. -/

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