closure_inter

Mathlib.Topology.Neighborhoods

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

English

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

Русский

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

LaTeX

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

Lean4

theorem closure_inter (h : IsOpen t) : closure s ∩ t ⊆ closure (s ∩ t) := by
  simpa only [inter_comm t] using h.inter_closure

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

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

Разделы

Аффилиация

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