continuous

Mathlib.Geometry.Manifold.ContMDiff.Defs

URI: https://scilib.ai/kg/mathlib#ContMDiff.continuous

English

From ContMDiffAt for n+1 to ContMDiffAt for n in the At sense.

Русский

Из ContMDiffAt для n+1 в ContMDiffAt для n.

LaTeX

$$ContMDiffAt I I' (n+1) f x \Rightarrow ContMDiffAt I I' n f x$$

Lean4

theorem continuous (hf : ContMDiff I I' n f) : Continuous f :=
  continuous_iff_continuousAt.2 fun x => (hf x).continuousAt

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

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

Разделы

Аффилиация

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