isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ

English

A local diffeomorphism is locally a diffeomorphism at every point; equivalently, being a local diffeomorphism on the whole space is the same as being so on every point.

Русский

Локальный диффеоморфизм по существу в каждой точке локален; эквивалентно тому, что он локально диффеоморфизм на всём пространстве и на каждой точке.

LaTeX

$$$ IsLocalDiffeomorph I J n f \iff IsLocalDiffeomorphOn I J n f Set.univ $$$

Lean4

theorem isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ {f : M → N} :
    IsLocalDiffeomorph I J n f ↔ IsLocalDiffeomorphOn I J n f Set.univ :=
  ⟨fun hf x ↦ hf x, fun hf x ↦ hf ⟨x, trivial⟩⟩

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