ordConnected_of_uIcc_subset_left — Mathlib

English

If every interval [[x,y]] with y ∈ s lies in s for all y ∈ s, then s is OrdConnected.

Русский

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

LaTeX

$$$\\bigl(\\forall y\\in s, [[x,y]] \\subseteq s\\bigr) \\Rightarrow \\operatorname{OrdConnected}(s)$$$

Lean4

theorem ordConnected_of_uIcc_subset_left (h : ∀ y ∈ s, [[x, y]] ⊆ s) : OrdConnected s :=
  ordConnected_iff_uIcc_subset.2 fun y hy z hz =>
    calc
      [[y, z]] ⊆ [[y, x]] ∪ [[x, z]] := uIcc_subset_uIcc_union_uIcc
      _ = [[x, y]] ∪ [[x, z]] := by rw [uIcc_comm]
      _ ⊆ s := union_subset (h y hy) (h z hz)

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