out

Mathlib.Order.Interval.Set.OrdConnected

URI: https://scilib.ai/kg/mathlib#Set.OrdConnected.out

English

If s is OrdConnected, then for any x,y ∈ s, Icc(x,y) ⊆ s.

Русский

Если s упорядочно связно, то для любых x,y ∈ s отрезок [x,y] ⊆ s.

LaTeX

$$$\forall x \in s\, \forall y \in s, \ Icc(x,y) \subseteq s.$$$

Lean4

theorem out (h : OrdConnected s) : ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), Icc x y ⊆ s :=
  h.1

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

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

Разделы

Аффилиация

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