disjoint_right_ordSeparatingSet

Mathlib.Order.Interval.Set.OrdConnectedComponent

URI: https://scilib.ai/kg/mathlib#Set.disjoint_right_ordSeparatingSet

English

Disjoint s and ordSeparatingSet(s,t).

Русский

Множество s и ordSeparatingSet(s,t) не пересекаются.

LaTeX

$$Disjoint(s, ordSeparatingSet(s,t))$$

Lean4

theorem disjoint_right_ordSeparatingSet : Disjoint t (ordSeparatingSet s t) :=
  ordSeparatingSet_comm t s ▸ disjoint_left_ordSeparatingSet

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

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

Разделы

Аффилиация

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