inter_of_isOpen_right

Mathlib.Topology.Neighborhoods

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

← MathLib Explorer

English

If s is dense, t is dense, and t is open, then s ∩ t is dense.

Русский

Если s плотное, t плотное, и t открыто, то s ∩ t плотное.

LaTeX

$$$\\text{Dense}(s \\cap t)$$$

Lean4

/-- The intersection of a dense set with an open dense set is a dense set. -/
theorem inter_of_isOpen_right (hs : Dense s) (ht : Dense t) (hto : IsOpen t) : Dense (s ∩ t) :=
  inter_comm t s ▸ ht.inter_of_isOpen_left hs hto

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

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

Разделы

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

Аффилиация

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