mathlib documentation

data.set.intervals.ord_connected

Order-connected sets

We say that a set s : set α is ord_connected if for all x y ∈ s it includes the interval [x, y]. If α is a densely_ordered conditionally_complete_linear_order with the order_topology, then this condition is equivalent to is_preconnected s. If α = ℝ, then this condition is also equivalent to convex s.

In this file we prove that intersection of a family of ord_connected sets is ord_connected and that all standard intervals are ord_connected.

@[class]
def set.ord_connected {α : Type u_1} [preorder α] :
set α → Prop

We say that a set s : set α is ord_connected if for all x y ∈ s it includes the interval [x, y]. If α is a densely_ordered conditionally_complete_linear_order with the order_topology, then this condition is equivalent to is_preconnected s. If α = ℝ, then this condition is also equivalent to convex s.

Equations
Instances
theorem set.ord_connected_iff {α : Type u_1} [preorder α] {s : set α} :
s.ord_connected ∀ (x : α), x s∀ (y : α), y sx yset.Icc x y s

It suffices to prove [x, y] ⊆ s for x y ∈ s, x ≤ y.

theorem set.ord_connected_of_Ioo {α : Type u_1} [partial_order α] {s : set α} :
(∀ (x : α), x s∀ (y : α), y sx < yset.Ioo x y s) → s.ord_connected

theorem set.ord_connected.inter {α : Type u_1} [preorder α] {s t : set α} :

theorem set.ord_connected.dual {α : Type u_1} [preorder α] {s : set α} :

theorem set.ord_connected_dual {α : Type u_1} [preorder α] {s : set α} :

theorem set.ord_connected_sInter {α : Type u_1} [preorder α] {S : set (set α)} :
(∀ (s : set α), s S → s.ord_connected) → (⋂₀S).ord_connected

theorem set.ord_connected_Inter {α : Type u_1} [preorder α] {ι : Sort u_2} {s : ι → set α} :
(∀ (i : ι), (s i).ord_connected)(⋂ (i : ι), s i).ord_connected

theorem set.ord_connected_bInter {α : Type u_1} [preorder α] {ι : Sort u_2} {p : ι → Prop} {s : Π (i : ι), p iset α} :
(∀ (i : ι) (hi : p i), (s i hi).ord_connected)(⋂ (i : ι) (hi : p i), s i hi).ord_connected

@[instance]
theorem set.ord_connected_Ici {α : Type u_1} [preorder α] {a : α} :

@[instance]
theorem set.ord_connected_Iic {α : Type u_1} [preorder α] {a : α} :

@[instance]
theorem set.ord_connected_Ioi {α : Type u_1} [preorder α] {a : α} :

@[instance]
theorem set.ord_connected_Iio {α : Type u_1} [preorder α] {a : α} :

@[instance]
theorem set.ord_connected_Icc {α : Type u_1} [preorder α] {a b : α} :

@[instance]
theorem set.ord_connected_Ico {α : Type u_1} [preorder α] {a b : α} :

@[instance]
theorem set.ord_connected_Ioc {α : Type u_1} [preorder α] {a b : α} :

@[instance]
theorem set.ord_connected_Ioo {α : Type u_1} [preorder α] {a b : α} :

theorem set.ord_connected_singleton {α : Type u_1} [partial_order α] {a : α} :

theorem set.ord_connected_empty {α : Type u_1} [preorder α] :

theorem set.ord_connected_univ {α : Type u_1} [preorder α] :

@[instance]
def set.densely_ordered {α : Type u_1} [preorder α] [densely_ordered α] {s : set α} [hs : s.ord_connected] :

In a dense order α, the subtype from an ord_connected set is also densely ordered.

theorem set.ord_connected_interval {β : Type u_2} [linear_order β] {a b : β} :

theorem set.ord_connected.interval_subset {β : Type u_2} [linear_order β] {s : set β} (hs : s.ord_connected) ⦃x : β⦄ (hx : x s) ⦃y : β⦄ :
y sset.interval x y s

theorem set.ord_connected_iff_interval_subset {β : Type u_2} [linear_order β] {s : set β} :
s.ord_connected ∀ ⦃x : β⦄, x s∀ ⦃y : β⦄, y sset.interval x y s