frontier_right

Mathlib.Topology.Closure

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

English

If s is open and s ∩ t = ∅, then s is disjoint from frontier(t).

Русский

Если s открыто и s ∩ t = ∅, то s не пересекается с frontier(t).

LaTeX

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

Lean4

theorem frontier_right (hs : IsOpen s) (hd : Disjoint s t) : Disjoint s (frontier t) :=
  (hd.symm.frontier_left hs).symm

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

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

Разделы

Аффилиация

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