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 α] (s : 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

s.ord_connected = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → set.Icc x y ⊆ s

Instances

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

s.ord_connected ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≤ y → set.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 α} (hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → set.Ioo x y ⊆ s) :

s.ord_connected

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

(s ∩ t).ord_connected

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

s.ord_connected

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

s.ord_connected ↔ s.ord_connected

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

(⋂₀S).ord_connected

theorem set.ord_connected_Inter {α : Type u_1} [preorder α] {ι : Sort u_2} {s : ι → set α} (hs : ∀ (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 i → set α} (hs : ∀ (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 : α} :

(set.Ici a).ord_connected

@[instance]

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

(set.Iic a).ord_connected

@[instance]

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

(set.Ioi a).ord_connected

@[instance]

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

(set.Iio a).ord_connected

@[instance]

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

(set.Icc a b).ord_connected

@[instance]

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

(set.Ico a b).ord_connected

@[instance]

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

(set.Ioc a b).ord_connected

@[instance]

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

(set.Ioo a b).ord_connected

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

{a}.ord_connected

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

∅.ord_connected

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

set.univ.ord_connected

@[instance]

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

densely_ordered ↥s

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

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

(set.interval a b).ord_connected

theorem set.ord_connected.interval_subset {β : Type u_2} [decidable_linear_order β] {s : set β} (hs : s.ord_connected) ⦃x : β⦄ (hx : x ∈ s) ⦃y : β⦄ (hy : y ∈ s) :

set.interval x y ⊆ s

theorem set.ord_connected_iff_interval_subset {β : Type u_2} [decidable_linear_order β] {s : set β} :

s.ord_connected ↔ ∀ ⦃x : β⦄, x ∈ s → ∀ ⦃y : β⦄, y ∈ s → set.interval x y ⊆ s