contMDiffAt_infty

Mathlib.Geometry.Manifold.ContMDiff.Defs

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

English

Relates ENat cast to Nat cast in the infinite case.

Русский

Связь ENat приведения к NAT-cast в бесконечном случае.

LaTeX

$$$ContMDiff I I' (WithTop.some instTopENat.top) f \iff ∀ n: \mathbb{N}, ContMDiff I I' n.cast f$$$

Lean4

theorem contMDiffAt_infty : ContMDiffAt I I' ∞ f x ↔ ∀ n : ℕ, ContMDiffAt I I' n f x :=
  contMDiffWithinAt_infty

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

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

Разделы

Аффилиация

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