ordConnected

Mathlib.Order.UpperLower.Basic

URI: https://scilib.ai/kg/mathlib#IsLowerSet.ordConnected

English

If s is lower, then s is order-connected: whenever a ≤ x ≤ b with a,b ∈ s, we have x ∈ s.

Русский

Если s — нижнее множество, то оно ордер-связано: если a ≤ x ≤ b и a,b ∈ s, то x ∈ s.

LaTeX

$$$IsLowerSet s \\to s.OrdConnected$$$

Lean4

theorem ordConnected (h : IsLowerSet s) : s.OrdConnected :=
  ⟨fun _ _ _ hb => Icc_subset_Iic_self.trans <| h.Iic_subset hb⟩

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

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

Разделы

Аффилиация

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