ordConnected_of_Ioo — Mathlib

English

If every open interval between any two points of s lies in s, then s is OrdConnected.

Русский

Если для любых x<y в s выполняется Ioo(x,y) ⊆ s, то s является OrdConnected.

LaTeX

$$$\bigl( \forall x \in s, \forall y \in s, x < y \Rightarrow \mathrm{Ioo}(x,y) \subseteq s \bigr) \Rightarrow \operatorname{OrdConnected}(s).$$$

Lean4

theorem ordConnected_of_Ioo {α : Type*} [PartialOrder α] {s : Set α} (hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s) :
    OrdConnected s := by
  rw [ordConnected_iff]
  intro x hx y hy hxy
  rcases eq_or_lt_of_le hxy with (rfl | hxy'); · simpa
  rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']
  exact insert_subset_iff.2 ⟨hx, insert_subset_iff.2 ⟨hy, hs x hx y hy hxy'⟩⟩

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