nhdsWithin_source_inter

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.nhdsWithin_source_inter

← MathLib Explorer

English

For x in the source, the nhds within e.source ∩ s equals the nhds within s.

Русский

Для x из источника, 𝓝[ e.source ∩ s ] x = 𝓝[ s ] x.

LaTeX

$$$\forall x\in e.source, 𝓝[e.source \cap s] x = 𝓝[s] x$$$

Lean4

theorem nhdsWithin_source_inter {x} (hx : x ∈ e.source) (s : Set X) : 𝓝[e.source ∩ s] x = 𝓝[s] x :=
  nhdsWithin_inter_of_mem (mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds e.open_source hx)

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

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

Разделы

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

Аффилиация

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