continuousOn_extChartAt

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

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

English

The map extChartAt I x is continuous on its source.

Русский

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

LaTeX

$$$ ContinuousOn\\ (\\mathrm{extChartAt} I x)\\ ((\\mathrm{extChartAt} I x).\\mathrm{source})$$$

Lean4

theorem continuousOn_extChartAt (x : M) : ContinuousOn (extChartAt I x) (extChartAt I x).source :=
  continuousOn_extend _

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

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

Разделы

Аффилиация

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