congr_iff

Mathlib.Geometry.Manifold.LocalInvariantProperties

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

← MathLib Explorer

English

For any h, P f s x ↔ P g s x when f =ᶠ[𝓝 x] g.

Русский

Для любого h, P f s x эквивалентно P g s x, если f и g совпадают в окрестности x.

LaTeX

$$$P f s x \iff P g s x \text{ when } f =ᶠ[\mathcal{N}x] g$$$

Lean4

theorem congr_iff {s : Set H} {x : H} {f g : H → H'} (h : f =ᶠ[𝓝 x] g) : P f s x ↔ P g s x :=
  hG.congr_iff_nhdsWithin (mem_nhdsWithin_of_mem_nhds h) (mem_of_mem_nhds h :)

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

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

Разделы

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

Аффилиация

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