nhdsWithin_restrict'

Mathlib.Topology.ContinuousOn

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

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 : t ∈ 𝓝 a) : 𝓝[s] a = 𝓝[s ∩ t] a :=
  nhdsWithin_restrict'' s <| mem_inf_of_left h

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

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

Разделы

Аффилиация

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