ordConnected_iff — Mathlib

English

OrdConnected s is equivalent to the property that between any two points of s, the closed interval lies in s.

Русский

OrdConnected s эквивалентно свойству: между любыми двумя точками множества отрезок [x,y] лежит в s.

LaTeX

$$$\operatorname{OrdConnected}(s) \iff \forall x \in s, \forall y \in s, \ x \le y \Rightarrow \mathrm{Icc}(x,y) \subseteq s.$$$

Lean4

/-- It suffices to prove `[[x, y]] ⊆ s` for `x y ∈ s`, `x ≤ y`. -/
theorem ordConnected_iff : OrdConnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s :=
  ordConnected_def.trans ⟨fun hs _ hx _ hy _ => hs hx hy, fun H x hx y hy _ hz => H x hx y hy (le_trans hz.1 hz.2) hz⟩

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