continuousOn_extChartAt_symm

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

URI: https://scilib.ai/kg/mathlib#continuousOn_extChartAt_symm

← MathLib Explorer

English

The map extChartAt I x .symm is continuous on its target set.

Русский

Карта extChartAt I x .symm непрерывна на своей целевой области.

LaTeX

$$$ \\text{ContinuousOn}((extChartAt I x).symm, (extChartAt I x).target)$$$

Lean4

theorem continuousOn_extChartAt_symm (x : M) : ContinuousOn (extChartAt I x).symm (extChartAt I x).target :=
  fun _y hy => (continuousAt_extChartAt_symm'' hy).continuousWithinAt

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

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

Разделы

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

Аффилиация

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