instOrdConnectedOrdConnectedComponent

Mathlib.Order.Interval.Set.OrdConnectedComponent

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

English

The set ordConnectedComponent(s, x) is order-connected.

Русский

Множество ordConnectedComponent(s, x) является упорядоченно связным.

LaTeX

$$$\operatorname{OrdConnected}(\operatorname{ordConnectedComponent}(s, x))$$$

Lean4

instance : OrdConnected (ordConnectedComponent s x) :=
  ordConnected_of_uIcc_subset_left fun _ hy _ hz => (uIcc_subset_uIcc_left hz).trans hy

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

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

Разделы

Аффилиация

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