mathlib3 documentation

data.set.intervals.ord_connected

Order-connected sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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 s set.Icc x y s
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) :
theorem set.ord_connected.preimage_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} {f : β α} (hs : s.ord_connected) (hf : monotone f) :
theorem set.ord_connected.preimage_anti {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} {f : β α} (hs : s.ord_connected) (hf : antitone f) :
@[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_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 i set α} (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]
@[instance]
@[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_preimage {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {F : Type u_3} [order_hom_class F α β] (f : F) {s : set β} [hs : s.ord_connected] :
@[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]
@[protected]
theorem is_antichain.ord_connected {α : Type u_1} [partial_order α] {s : set α} (hs : is_antichain has_le.le s) :
@[instance]
theorem set.ord_connected_uIcc {α : Type u_1} [linear_order α] {a b : α} :
@[instance]
theorem set.ord_connected_uIoc {α : Type u_1} [linear_order α] {a b : α} :
theorem set.ord_connected.uIcc_subset {α : Type u_1} [linear_order α] {s : set α} (hs : s.ord_connected) ⦃x : α⦄ (hx : x s) ⦃y : α⦄ (hy : y s) :
theorem set.ord_connected.uIoc_subset {α : Type u_1} [linear_order α] {s : set α} (hs : s.ord_connected) ⦃x : α⦄ (hx : x s) ⦃y : α⦄ (hy : y s) :
theorem set.ord_connected_iff_uIcc_subset {α : Type u_1} [linear_order α] {s : set α} :
s.ord_connected ⦃x : α⦄, x s ⦃y : α⦄, y s set.uIcc x y s
theorem set.ord_connected_of_uIcc_subset_left {α : Type u_1} [linear_order α] {s : set α} {x : α} (h : (y : α), y s set.uIcc x y s) :
theorem set.ord_connected_iff_uIcc_subset_left {α : Type u_1} [linear_order α] {s : set α} {x : α} (hx : x s) :
s.ord_connected ⦃y : α⦄, y s set.uIcc x y s
theorem set.ord_connected_iff_uIcc_subset_right {α : Type u_1} [linear_order α] {s : set α} {x : α} (hx : x s) :
s.ord_connected ⦃y : α⦄, y s set.uIcc y x s