ordConnectedComponent_subset

Mathlib.Order.Interval.Set.OrdConnectedComponent

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

English

The union-closed interval uIcc is OrdConnected.

Русский

Объединённый интервал uIcc упорядоченно связан.

LaTeX

$$$\\operatorname{OrdConnected}([[a,b]])$$$

Lean4

theorem ordConnectedComponent_subset : ordConnectedComponent s x ⊆ s := fun _ hy => hy right_mem_uIcc

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

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

Разделы

Аффилиация

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