localInverse_mem_target

Mathlib.Geometry.Manifold.LocalDiffeomorph

URI: https://scilib.ai/kg/mathlib#IsLocalDiffeomorphAt.localInverse_mem_target

English

The image under the local inverse of the point lies in the source.

Русский

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

LaTeX

$$hf.localInverse.source contains f(x)$$

Lean4

theorem localInverse_mem_target (hf : IsLocalDiffeomorphAt I J n f x) : x ∈ hf.localInverse.target :=
  hf.choose_spec.1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru