ordConnectedComponent_empty

Mathlib.Order.Interval.Set.OrdConnectedComponent

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

English

For every x, the order-connected component of the empty set at x is the empty set.

Русский

Для любого x ор connected-компонента пустого множества при x равна пустому множеству.

LaTeX

$$$\operatorname{ordConnectedComponent}(\emptyset, x) = \emptyset$$$

Lean4

@[simp]
theorem ordConnectedComponent_empty : ordConnectedComponent ∅ x = ∅ :=
  ordConnectedComponent_eq_empty.2 (notMem_empty x)

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

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

Разделы

Аффилиация

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