continuousAt_extChartAt

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

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

English

The map extChartAt I x is continuous at x.

Русский

Карта extChartAt I x непрерывна в x.

LaTeX

$$$ ContinuousAt (\\mathrm{extChartAt} I x) x$$$

Lean4

theorem continuousAt_extChartAt (x : M) : ContinuousAt (extChartAt I x) x :=
  continuousAt_extChartAt' (mem_extChartAt_source x)

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

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

Разделы

Аффилиация

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