Intervals

In any preorder α, we define intervals (which on each side can be either infinite, open, or closed) using the following naming conventions:

• i: infinite
• o: open
• c: closed

Each interval has the name I + letter for left side + letter for right side. For instance, Ioc a b denotes the interval (a, b].

We also define a typeclass Set.OrdConnected saying that a set includes Set.Icc a b whenever it contains both a and b.

def Set.Ioo {α : Type u_1} [Preorder α] (a b : α) : Set α

Ioo a b is the left-open right-open interval $(a, b)$.

@[simp]

theorem Set.mem_Ioo {α : Type u_1} [Preorder α] {a b x : α} : x ∈ Ioo a b ↔ a < x ∧ x < b

theorem Set.Ioo_def {α : Type u_1} [Preorder α] (a b : α) : {x : α | a < x ∧ x < b} = Ioo a b

def Set.Ico {α : Type u_1} [Preorder α] (a b : α) : Set α

Ico a b is the left-closed right-open interval $[a, b)$.

@[simp]

theorem Set.mem_Ico {α : Type u_1} [Preorder α] {a b x : α} : x ∈ Ico a b ↔ a ≤ x ∧ x < b

theorem Set.Ico_def {α : Type u_1} [Preorder α] (a b : α) : {x : α | a ≤ x ∧ x < b} = Ico a b

def Set.Iio {α : Type u_1} [Preorder α] (b : α) : Set α

Iio b is the left-infinite right-open interval $(-∞, b)$.

@[simp]

theorem Set.mem_Iio {α : Type u_1} [Preorder α] {b x : α} : x ∈ Iio b ↔ x < b

theorem Set.Iio_def {α : Type u_1} [Preorder α] (a : α) : {x : α | x < a} = Iio a

def Set.Icc {α : Type u_1} [Preorder α] (a b : α) : Set α

Icc a b is the left-closed right-closed interval $[a, b]$.

@[simp]

theorem Set.mem_Icc {α : Type u_1} [Preorder α] {a b x : α} : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

theorem Set.Icc_def {α : Type u_1} [Preorder α] (a b : α) : {x : α | a ≤ x ∧ x ≤ b} = Icc a b

def Set.Iic {α : Type u_1} [Preorder α] (b : α) : Set α

Iic b is the left-infinite right-closed interval $(-∞, b]$.

@[simp]

theorem Set.mem_Iic {α : Type u_1} [Preorder α] {b x : α} : x ∈ Iic b ↔ x ≤ b

theorem Set.Iic_def {α : Type u_1} [Preorder α] (b : α) : {x : α | x ≤ b} = Iic b

def Set.Ioc {α : Type u_1} [Preorder α] (a b : α) : Set α

Ioc a b is the left-open right-closed interval $(a, b]$.

@[simp]

theorem Set.mem_Ioc {α : Type u_1} [Preorder α] {a b x : α} : x ∈ Ioc a b ↔ a < x ∧ x ≤ b

theorem Set.Ioc_def {α : Type u_1} [Preorder α] (a b : α) : {x : α | a < x ∧ x ≤ b} = Ioc a b

def Set.Ici {α : Type u_1} [Preorder α] (a : α) : Set α

Ici a is the left-closed right-infinite interval $[a, ∞)$.

@[simp]

theorem Set.mem_Ici {α : Type u_1} [Preorder α] {a x : α} : x ∈ Ici a ↔ a ≤ x

theorem Set.Ici_def {α : Type u_1} [Preorder α] (a : α) : {x : α | a ≤ x} = Ici a

def Set.Ioi {α : Type u_1} [Preorder α] (a : α) : Set α

Ioi a is the left-open right-infinite interval $(a, ∞)$.

@[simp]

theorem Set.mem_Ioi {α : Type u_1} [Preorder α] {a x : α} : x ∈ Ioi a ↔ a < x

theorem Set.Ioi_def {α : Type u_1} [Preorder α] (a : α) : {x : α | a < x} = Ioi a

class Set.OrdConnected {α : Type u_1} [Preorder α] (s : Set α) : Prop

We say that a set s : Set α is OrdConnected if for all x y ∈ s it includes the interval [[x, y]]. If α is a DenselyOrdered ConditionallyCompleteLinearOrder with the OrderTopology, then this condition is equivalent to IsPreconnected s. If α is a LinearOrderedField, then this condition is also equivalent to Convex α s.

• out' ⦃x : α⦄ (hx : x ∈ s) ⦃y : α⦄ (hy : y ∈ s) : Icc x y ⊆ s

  s : Set α is OrdConnected if for all x y ∈ s it includes the interval [[x, y]].