localInverse_mem_source

Mathlib.Geometry.Manifold.LocalDiffeomorph

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

← MathLib Explorer

English

f x belongs to the target of the local inverse.

Русский

f x принадлежит области определения локального обратного.

LaTeX

$$f x ∈ hf.localInverse.target$$

Lean4

theorem localInverse_mem_source (hf : IsLocalDiffeomorphAt I J n f x) : f x ∈ hf.localInverse.source :=
  by
  rw [(hf.choose_spec.2 hf.choose_spec.1)]
  exact (Classical.choose hf).map_source hf.choose_spec.1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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