inter_closure

Mathlib.Topology.Neighborhoods

URI: https://scilib.ai/kg/mathlib#IsOpen.inter_closure

← MathLib Explorer

English

If s is open, then s ∩ closure(t) ⊆ closure(s ∩ t).

Русский

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

LaTeX

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

Lean4

theorem inter_closure (h : IsOpen s) : s ∩ closure t ⊆ closure (s ∩ t) :=
  compl_subset_compl.mp <| by
    simpa only [← interior_compl, compl_inter] using IsClosed.interior_union_left h.isClosed_compl

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

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

Разделы

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

Аффилиация

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