nhdsWithin_eq_nhdsWithin'

Mathlib.Topology.ContinuousOn

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

← MathLib Explorer

English

If hs is in nhds a and t ∩ s = u ∩ s, then 𝓝[t] a = 𝓝[u] a.

Русский

Если hs ∈ nhds a и t ∩ s = u ∩ s, тогда 𝓝[t] a = 𝓝[u] a.

LaTeX

$$$ \mathcal{N}_t(a) = \mathcal{N}_u(a) $$$

Lean4

theorem nhdsWithin_eq_nhdsWithin' {a : α} {s t u : Set α} (hs : s ∈ 𝓝 a) (h₂ : t ∩ s = u ∩ s) : 𝓝[t] a = 𝓝[u] a := by
  rw [nhdsWithin_restrict' t hs, nhdsWithin_restrict' u hs, h₂]

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

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

Разделы

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

Аффилиация

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