congr_nhdsWithin'

Mathlib.Geometry.Manifold.LocalInvariantProperties

URI: https://scilib.ai/kg/mathlib#StructureGroupoid.LocalInvariantProp.congr_nhdsWithin'

← MathLib Explorer

English

Reiterates the coe relation for mfderiv in local coordinates.

Русский

Повторное утверждение соотношения коэ mfderiv в локальных координатах.

LaTeX

$$(hf : IsLocalDiffeomorph I J n f) (hn : 1 ≤ n) x :$$

Lean4

theorem congr_nhdsWithin' {s : Set H} {x : H} {f g : H → H'} (h1 : f =ᶠ[𝓝[s] x] g) (h2 : f x = g x) (hP : P g s x) :
    P f s x :=
  (hG.congr_iff_nhdsWithin h1 h2).mpr hP

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

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

Разделы

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

Аффилиация

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