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)$.

Equations

• Set.Ioo a b = {x : α | a < x ∧ x < b}

@[simp]

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

theorem Set.Ioo_def {α : Type u_1} [Preorder α] (a : α) (b : α) : {x : α | a < x ∧ x < b} = Set.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)$.

Equations

• Set.Ico a b = {x : α | a ≤ x ∧ x < b}

@[simp]

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

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

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

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

Equations

• Set.Iio b = {x : α | x < b}

@[simp]

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

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

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

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

Equations

• Set.Icc a b = {x : α | a ≤ x ∧ x ≤ b}

@[simp]

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

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

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

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

Equations

• Set.Iic b = {x : α | x ≤ b}

@[simp]

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

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

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

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

Equations

• Set.Ioc a b = {x : α | a < x ∧ x ≤ b}

@[simp]

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

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

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

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

Equations

• Set.Ici a = {x : α | a ≤ x}

@[simp]

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

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

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

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

Equations

• Set.Ioi a = {x : α | a < x}

@[simp]

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

theorem Set.Ioi_def {α : Type u_1} [Preorder α] (a : α) : {x : α | a < x} = Set.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 : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s

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

theorem Set.OrdConnected.out' {α : Type u_1} : ∀ {inst : Preorder α} {s : Set α} [self : s.OrdConnected] ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s

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