Documentation

Mathlib.Order.Interval.Set.Defs

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}

Instances For

Set.ordConnected_Ioo

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

Equations

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

Instances For

Set.ordConnected_Ico

@[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 $(- \infty, b)$ .

Equations

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

Instances For

Set.ordConnected_Iio

@[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]$ .

Equations

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

Instances For

Set.ordConnected_Icc

@[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 $(- \infty, b]$ .

Equations

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

Instances For

Set.ordConnected_Iic

@[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]$ .

Equations

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

Instances For

Set.ordConnected_Ioc

@[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, \infty)$ .

Equations

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

Instances For

Set.ordConnected_Ici

@[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, \infty)$ .

Equations

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

Instances For

Set.ordConnected_Ioi

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

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]].

Instances