is_local_nhds

Mathlib.Geometry.Manifold.LocalInvariantProperties

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

← MathLib Explorer

English

If s and u are neighborhood-related near x, then P f s x ↔ P f (s ∩ u) x.

Русский

Если s и u относятся как окрестности около x, то P f s x эквивалентно P f (s ∩ u) x.

LaTeX

$$$P f s x \iff P f (s \cap u) x$ for u ∈ 𝓝[x] s$$

Lean4

theorem is_local_nhds {s u : Set H} {x : H} {f : H → H'} (hu : u ∈ 𝓝[s] x) : P f s x ↔ P f (s ∩ u) x :=
  hG.congr_set <| mem_nhdsWithin_iff_eventuallyEq.mp hu

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

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

Разделы

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

Аффилиация

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