image

Mathlib.Geometry.Manifold.LocalDiffeomorph

URI: https://scilib.ai/kg/mathlib#IsLocalDiffeomorph.image

English

The image of a local diffeomorphism is open.

Русский

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

LaTeX

$$$hf.image \in Opens N$$$

Lean4

/-- The image of a local diffeomorphism is open. -/
def image (hf : IsLocalDiffeomorph I J n f) : Opens N :=
  ⟨range f, hf.isOpen_range⟩

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

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

Разделы

Аффилиация

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