continuousWithinAt

Mathlib.Geometry.Manifold.ContMDiff.Defs

URI: https://scilib.ai/kg/mathlib#ContMDiffWithinAt.continuousWithinAt

English

From ContMDiffOn for n+1 to ContMDiffOn for n, given the local chart extension property.

Русский

Из ContMDiffOn на n+1 следует ContMDiffOn на n с учетом локального расширения диаграмм.

LaTeX

$$$ContMDiffOn I I' (n+1) f s \Rightarrow ContMDiffOn I I' n f s$$$

Lean4

theorem continuousWithinAt (hf : ContMDiffWithinAt I I' n f s x) : ContinuousWithinAt f s x :=
  hf.1

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

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

Разделы

Аффилиация

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