contMDiffAt_comp_diffeomorph_iff

Mathlib.Geometry.Manifold.Diffeomorph

URI: https://scilib.ai/kg/mathlib#Diffeomorph.contMDiffAt_comp_diffeomorph_iff

← MathLib Explorer

English

The underlying function of h.toHomeomorph equals h.

Русский

Базовая функция h.toHomeomorph совпадает с h.

LaTeX

$$$\\uparrow(h^{\\text{Homeomorph}}) = h$$$

Lean4

@[simp]
theorem contMDiffAt_comp_diffeomorph_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : N → M'} {x} (hm : m ≤ n) :
    ContMDiffAt I I' m (f ∘ h) x ↔ ContMDiffAt J I' m f (h x) :=
  h.contMDiffWithinAt_comp_diffeomorph_iff hm

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

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

Разделы

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

Аффилиация

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