nhdsWithin_restrict

Mathlib.Topology.ContinuousOn

URI: https://scilib.ai/kg/mathlib#nhdsWithin_restrict

← MathLib Explorer

English

If t is a neighborhood of a (in the ambient space), then 𝓝[s] a = 𝓝[s ∩ t] a.

Русский

Если t является окрестностью a в окружении, то 𝓝[s] a = 𝓝[s ∩ t] a.

LaTeX

$$$ \mathcal{N}_s(a) = \mathcal{N}_{s \cap t}(a) $$$

Lean4

theorem nhdsWithin_restrict {a : α} (s : Set α) {t : Set α} (h₀ : a ∈ t) (h₁ : IsOpen t) : 𝓝[s] a = 𝓝[s ∩ t] a :=
  nhdsWithin_restrict' s (IsOpen.mem_nhds h₁ h₀)

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

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

Разделы

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

Аффилиация

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