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 α is a linear_ordered_field, 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]
structure set.ord_connected {α : Type u_1} [preorder α] (s : set α) :
Prop
  • out' : ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sset.Icc x y s

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 α is a linear_ordered_field, then this condition is also equivalent to convex α s.

Instances
theorem set.ord_connected.out {α : Type u_1} [preorder α] {s : set α} (h : s.ord_connected) ⦃x : α⦄ (hx : x s) ⦃y : α⦄ (hy : y s) :
set.Icc x y s
theorem set.ord_connected_def {α : Type u_1} [preorder α] {s : set α} :
s.ord_connected ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sset.Icc x y s
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 α} (hs : ∀ (x : α), x s∀ (y : α), y sx < yset.Ioo x y s) :
@[protected]
theorem set.Icc_subset {α : Type u_1} [preorder α] (s : set α) [hs : s.ord_connected] {x y : α} (hx : x s) (hy : y s) :
set.Icc x y s
theorem set.ord_connected.inter {α : Type u_1} [preorder α] {s t : set α} (hs : s.ord_connected) (ht : t.ord_connected) :
@[protected, instance]
def set.ord_connected.inter' {α : Type u_1} [preorder α] {s t : set α} [s.ord_connected] [t.ord_connected] :
theorem set.ord_connected.dual {α : Type u_1} [preorder α] {s : set α} (hs : s.ord_connected) :
theorem set.ord_connected_sInter {α : Type u_1} [preorder α] {S : set (set α)} (hS : ∀ (s : set α), s S → 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
@[protected, instance]
def 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 α} (hs : ∀ (i : ι) (hi : p i), (s i hi).ord_connected) :
(⋂ (i : ι) (hi : p i), s i hi).ord_connected
theorem set.ord_connected_pi {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), preorder (α i)] {s : set ι} {t : Π (i : ι), set (α i)} (h : ∀ (i : ι), i s(t i).ord_connected) :
@[protected, instance]
def set.ord_connected_pi' {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), preorder (α i)] {s : set ι} {t : Π (i : ι), set (α i)} [h : ∀ (i : ι), (t i).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 : α} :
@[instance]
theorem set.ord_connected_singleton {α : Type u_1} [partial_order α] {a : α} :
@[instance]
theorem set.ord_connected_empty {α : Type u_1} [preorder α] :
@[instance]
theorem set.ord_connected_univ {α : Type u_1} [preorder α] :
@[protected, 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.

@[instance]
theorem set.ord_connected_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {E : Type u_3} [order_iso_class E α β] (e : E) {s : set α} [hs : s.ord_connected] :
@[instance]
theorem set.ord_connected_range {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {E : Type u_3} [order_iso_class E α β] (e : E) :
@[instance]
theorem set.ord_connected_interval {α : Type u_1} [linear_order α] {a b : α} :
theorem set.ord_connected.interval_subset {α : Type u_1} [linear_order α] {s : set α} (hs : s.ord_connected) ⦃x : α⦄ (hx : x s) ⦃y : α⦄ (hy : y s) :
[x, y] s
theorem set.ord_connected_iff_interval_subset {α : Type u_1} [linear_order α] {s : set α} :
s.ord_connected ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y s[x, y] s
theorem set.ord_connected_iff_interval_subset_left {α : Type u_1} [linear_order α] {s : set α} {x : α} (hx : x s) :
s.ord_connected ∀ ⦃y : α⦄, y s[x, y] s
theorem set.ord_connected_iff_interval_subset_right {α : Type u_1} [linear_order α] {s : set α} {x : α} (hx : x s) :
s.ord_connected ∀ ⦃y : α⦄, y s[y, x] s