continuousOn_extend

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.continuousOn_extend

← MathLib Explorer

English

The extended chart is continuous on its domain.

Русский

Расширенный чарт непрерывен на своей области определения.

LaTeX

$$$ \\text{ContinuousOn}(f^{\\mathrm{extend}}_I, (f^{\\mathrm{extend}}_I).\\mathrm{source}).$$$

Lean4

theorem continuousOn_extend : ContinuousOn (f.extend I) (f.extend I).source :=
  by
  refine I.continuous.comp_continuousOn ?_
  rw [extend_source]
  exact f.continuousOn

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

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

Разделы

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

Аффилиация

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