ordConnected_iff_uIcc_subset — Mathlib

English

For a point x in s, s is OrdConnected if and only if for all y ∈ s, [[x,y]] ⊆ s.

Русский

Для точки x∈s множество s упорядоченно связно тогда и только тогда, когда для всех y∈s выполняется [[x,y]] ⊆ s.

LaTeX

$$$\\forall x\\in s,\\ \\operatorname{OrdConnected}(s) \\iff \\forall y\\in s,\\ \\lbrack\\! [x,y] \\!\\rbrack \\subseteq s$$$

Lean4

theorem ordConnected_iff_uIcc_subset : OrdConnected s ↔ ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), [[x, y]] ⊆ s :=
  ⟨fun h => h.uIcc_subset, fun H => ⟨fun _ hx _ hy => Icc_subset_uIcc.trans <| H hx hy⟩⟩

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