contMDiffOn_congr

Mathlib.Geometry.Manifold.ContMDiff.Defs

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

← MathLib Explorer

English

A constant map is ContMDiffAt/ContMDiffOn for all i‑domains.

Русский

Постоянная карта является ContMDiffAt/ContMDiffOn для любых областей определения.

LaTeX

$$$ ContMDiff I I' n (fun _ : M => c)$$

Lean4

theorem contMDiffOn_congr (h₁ : ∀ y ∈ s, f₁ y = f y) : ContMDiffOn I I' n f₁ s ↔ ContMDiffOn I I' n f s :=
  (contDiffWithinAt_localInvariantProp n).liftPropOn_congr_iff h₁

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

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

Разделы

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

Аффилиация

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