closure_right

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#Disjoint.closure_right

English

If s and t are disjoint and s is open, then s is disjoint from closure(t).

Русский

Если s и t дизjoint и s открыто, то s дизjoint с closure(t).

LaTeX

$$Disjoint(s,t) \land IsOpen(s) \Rightarrow Disjoint(s, \overline{t})$$

Lean4

theorem closure_right (hd : Disjoint s t) (hs : IsOpen s) : Disjoint s (closure t) :=
  (hd.symm.closure_left hs).symm

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

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

Разделы

Аффилиация

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