isPreconnected — Mathlib

English

If a set is order-connected, then it is preconnected.

Русский

Если множество упорядочено и связано по порядку, тогда оно предсвязано.

LaTeX

$$$s.OrdConnected \Rightarrow IsPreconnected(s)$$$

Lean4

theorem isPreconnected {s : Set α} (h : s.OrdConnected) : IsPreconnected s :=
  isPreconnected_of_forall_pair fun x hx y hy =>
    ⟨[[x, y]], h.uIcc_subset hx hy, left_mem_uIcc, right_mem_uIcc, isPreconnected_uIcc⟩

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