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 ∈ s → set.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 ∈ 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) :

s.ord_connected

@[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) :

(s ∩ t).ord_connected

@[protected, instance]

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

(s ∩ t).ord_connected

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

(⇑order_dual.of_dual ⁻¹' s).ord_connected

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

(⇑order_dual.of_dual ⁻¹' 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

@[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) :

(s.pi t).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] :

(s.pi t).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

@[instance]

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

{a}.ord_connected

@[instance]

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

∅.ord_connected

@[instance]

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

set.univ.ord_connected

@[protected, 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.

@[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] :

(⇑e '' 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) :

(set.range ⇑e).ord_connected

@[instance]

theorem set.ord_connected_interval {α : Type u_1} [linear_order α] {a b : α} :

[a, b].ord_connected

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