open_subset_closure_inter

Mathlib.Topology.Neighborhoods

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

← MathLib Explorer

English

If s is dense and t is open, then t is contained in closure(t ∩ s).

Русский

Если s плотное, а t открыто, то t ⊆ closure(t ∩ s).

LaTeX

$$$t \\subseteq \\overline{(t \\cap s)}$$$

Lean4

theorem open_subset_closure_inter (hs : Dense s) (ht : IsOpen t) : t ⊆ closure (t ∩ s) :=
  calc
    t = t ∩ closure s := by rw [hs.closure_eq, inter_univ]
    _ ⊆ closure (t ∩ s) := ht.inter_closure

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

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

Разделы

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

Аффилиация

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