continuousOn

Mathlib.Geometry.Manifold.ContMDiff.Defs

URI: https://scilib.ai/kg/mathlib#ContMDiffOn.continuousOn

English

A function is C^n for ENat∞ if and only if it is C^n for every finite n.

Русский

Функция C^n для ENat∞ эквивалентна тому, что она C^n для каждого сколь угодно большого конечного n.

LaTeX

$$$ContMDiff I I' ∞ f \iff ∀ n: \mathbb{N}, ContMDiff I I' n f$$$

Lean4

theorem continuousOn (hf : ContMDiffOn I I' n f s) : ContinuousOn f s := fun x hx => (hf x hx).continuousWithinAt

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

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

Разделы

Аффилиация

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