isLocalDiffeomorph_iff — Mathlib

English

A map is a local diffeomorphism iff it is a local diffeomorphism at every point.

Русский

Отображение является локальным диффеоморфизмом тогда и только тогда, когда оно локально является диффеоморфизмом в каждой точке.

LaTeX

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

Lean4

theorem isLocalDiffeomorph_iff {f : M → N} : IsLocalDiffeomorph I J n f ↔ ∀ x : M, IsLocalDiffeomorphAt I J n f x := by
  rfl

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