inter_nhds_nonempty

Mathlib.Topology.Neighborhoods

URI: https://scilib.ai/kg/mathlib#Dense.inter_nhds_nonempty

← MathLib Explorer

English

If s is dense and t ∈ 𝓝 x, then (s ∩ t) is Nonempty.

Русский

Если s плотное и t ∈ 𝓝 x, то (s ∩ t) непусто.

LaTeX

$$$(s \\cap t).\\text{Nonempty}$$$

Lean4

theorem inter_nhds_nonempty (hs : Dense s) (ht : t ∈ 𝓝 x) : (s ∩ t).Nonempty :=
  let ⟨U, hsub, ho, hx⟩ := mem_nhds_iff.1 ht
  (hs.inter_open_nonempty U ho ⟨x, hx⟩).mono fun _y hy => ⟨hy.2, hsub hy.1⟩

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

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

Разделы

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

Аффилиация

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