congr_nhdsWithin

Mathlib.Geometry.Manifold.LocalInvariantProperties

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

← MathLib Explorer

English

If nhdsWithin-equivalence holds from nhds, then P f s x ↔ P f t x.

Русский

Если nhdsWithin-эквивалентность следует из nhds, то P f s x эквивалентно P f t x.

LaTeX

$$$P f s x \iff P f t x$ from nhds equivalence$$

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 f s x) :
    P g s x :=
  (hG.congr_iff_nhdsWithin h1 h2).mp hP

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

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

Разделы

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

Аффилиация

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