ordConnected_iff_uIcc_subset_right

English

For a point x in s, OrdConnected(s) is equivalent to for all y ∈ s, [[y,x]] ⊆ s.

Русский

Для x∈s OrdConnected(s) эквивалентно тому, что для всех y∈s выполняется [[y,x]] ⊆ s.

LaTeX

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

Lean4

theorem ordConnected_iff_uIcc_subset_right (hx : x ∈ s) : OrdConnected s ↔ ∀ ⦃y⦄, y ∈ s → [[y, x]] ⊆ s := by
  simp_rw [ordConnected_iff_uIcc_subset_left hx, uIcc_comm]

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