Mathlib.Order.Interval.Set.Defs

Set.Ioo definition

(a b : α)

Full source

/-- `Ioo a b` is the left-open right-open interval $(a, b)$. -/
def Ioo (a b : α) := { x | a < x ∧ x < b }

Open interval $(a, b)$

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, the interval $\text{Ioo}(a, b)$ is defined as the set of all elements $x$ such that $a < x < b$. This is the left-open right-open interval $(a, b)$.

Set.mem_Ioo theorem

: x ∈ Ioo a b ↔ a < x ∧ x < b

Full source

@[simp] theorem mem_Ioo : x ∈ Ioo a bx ∈ Ioo a b ↔ a < x ∧ x < b := Iff.rfl

Membership Criterion for Open Interval $(a, b)$

Informal description

For any elements $a$, $b$, and $x$ in a preorder $\alpha$, the element $x$ belongs to the open interval $(a, b)$ if and only if $a < x$ and $x < b$.

Set.Ioo_def theorem

(a b : α) : {x | a < x ∧ x < b} = Ioo a b

Full source

theorem Ioo_def (a b : α) : { x | a < x ∧ x < b } = Ioo a b := rfl

Definition of Open Interval via Set Comprehension: $\{x \mid a < x < b\} = (a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the set $\{x \mid a < x < b\}$ is equal to the open interval $\text{Ioo}(a, b)$.

Set.Ico definition

(a b : α)

Full source

/-- `Ico a b` is the left-closed right-open interval $[a, b)$. -/
def Ico (a b : α) := { x | a ≤ x ∧ x < b }

Left-closed right-open interval

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, the interval $\text{Ico}(a, b)$ is defined as the set of all elements $x$ such that $a \leq x < b$. This is a left-closed, right-open interval.

Set.mem_Ico theorem

: x ∈ Ico a b ↔ a ≤ x ∧ x < b

Full source

@[simp] theorem mem_Ico : x ∈ Ico a bx ∈ Ico a b ↔ a ≤ x ∧ x < b := Iff.rfl

Membership Criterion for Left-Closed Right-Open Interval

Informal description

For any elements $a$, $b$, and $x$ in a preorder $\alpha$, the element $x$ belongs to the interval $\text{Ico}(a, b)$ if and only if $a \leq x$ and $x < b$.

Set.Ico_def theorem

(a b : α) : {x | a ≤ x ∧ x < b} = Ico a b

Full source

theorem Ico_def (a b : α) : { x | a ≤ x ∧ x < b } = Ico a b := rfl

Characterization of Left-Closed Right-Open Interval as Set of Elements Between $a$ and $b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the set $\{x \mid a \leq x < b\}$ is equal to the left-closed right-open interval $\text{Ico}(a, b)$.

Set.Iio definition

(b : α)

Full source

/-- `Iio b` is the left-infinite right-open interval $(-∞, b)$. -/
def Iio (b : α) := { x | x < b }

Left-infinite right-open interval $(-\infty, b)$

Informal description

For an element $b$ in a preorder $\alpha$, the interval $\operatorname{Iio}(b)$ is defined as the set $\{x \mid x < b\}$, representing all elements less than $b$.

Set.mem_Iio theorem

: x ∈ Iio b ↔ x < b

Full source

@[simp] theorem mem_Iio : x ∈ Iio bx ∈ Iio b ↔ x < b := Iff.rfl

Membership in Left-Infinite Right-Open Interval: $x \in (-\infty, b) \leftrightarrow x < b$

Informal description

For any element $x$ in a preorder $\alpha$, $x$ belongs to the interval $(-\infty, b)$ if and only if $x < b$.

Set.Iio_def theorem

(a : α) : {x | x < a} = Iio a

Full source

theorem Iio_def (a : α) : { x | x < a } = Iio a := rfl

Characterization of $\operatorname{Iio}(a)$ as $\{x \mid x < a\}$

Informal description

For any element $a$ in a preorder $\alpha$, the set $\{x \mid x < a\}$ is equal to the left-infinite right-open interval $(-\infty, a)$, denoted as $\operatorname{Iio}(a)$.

Set.Icc definition

(a b : α)

Full source

/-- `Icc a b` is the left-closed right-closed interval $[a, b]$. -/
def Icc (a b : α) := { x | a ≤ x ∧ x ≤ b }

Closed interval $[a, b]$

Informal description

For elements $ a $ and $ b $ in a preorder $ \alpha $, the set $ \text{Icc}(a, b) $ is defined as the closed interval $[a, b]$, consisting of all elements $ x $ such that $ a \leq x \leq b $.

Set.mem_Icc theorem

: x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

Full source

@[simp] theorem mem_Icc : x ∈ Icc a bx ∈ Icc a b ↔ a ≤ x ∧ x ≤ b := Iff.rfl

Membership Criterion for Closed Interval $[a, b]$

Informal description

For any elements $a, b, x$ in a preorder $\alpha$, the element $x$ belongs to the closed interval $[a, b]$ if and only if $a \leq x$ and $x \leq b$.

Set.Icc_def theorem

(a b : α) : {x | a ≤ x ∧ x ≤ b} = Icc a b

Full source

theorem Icc_def (a b : α) : { x | a ≤ x ∧ x ≤ b } = Icc a b := rfl

Definition of Closed Interval via Set Comprehension

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the set $\{x \mid a \leq x \leq b\}$ is equal to the closed interval $[a, b]$.

Set.Iic definition

(b : α)

Full source

/-- `Iic b` is the left-infinite right-closed interval $(-∞, b]$. -/
def Iic (b : α) := { x | x ≤ b }

Left-infinite right-closed interval $ (-\infty, b] $

Informal description

For an element $ b $ in a preorder $ \alpha $, the set $ \text{Iic } b $ is defined as the left-infinite right-closed interval $ (-\infty, b] $, consisting of all elements $ x $ in $ \alpha $ such that $ x \leq b $.

Set.mem_Iic theorem

: x ∈ Iic b ↔ x ≤ b

Full source

@[simp] theorem mem_Iic : x ∈ Iic bx ∈ Iic b ↔ x ≤ b := Iff.rfl

Membership Criterion for Left-Infinite Right-Closed Interval: $x \in (-\infty, b] \leftrightarrow x \leq b$

Informal description

For an element $x$ in a preorder $\alpha$ and an element $b \in \alpha$, $x$ belongs to the left-infinite right-closed interval $(-\infty, b]$ if and only if $x \leq b$.

Set.Iic_def theorem

(b : α) : {x | x ≤ b} = Iic b

Full source

theorem Iic_def (b : α) : { x | x ≤ b } = Iic b := rfl

Characterization of Left-Infinite Right-Closed Interval as Lower Set

Informal description

For any element $b$ in a preorder $\alpha$, the set $\{x \mid x \leq b\}$ is equal to the left-infinite right-closed interval $(-\infty, b]$.

Set.Ioc definition

(a b : α)

Full source

/-- `Ioc a b` is the left-open right-closed interval $(a, b]$. -/
def Ioc (a b : α) := { x | a < x ∧ x ≤ b }

Left-open right-closed interval

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, the interval $\text{Ioc}(a, b)$ is defined as the set of all elements $x$ such that $a < x \leq b$. This is a left-open right-closed interval.

Set.mem_Ioc theorem

: x ∈ Ioc a b ↔ a < x ∧ x ≤ b

Full source

@[simp] theorem mem_Ioc : x ∈ Ioc a bx ∈ Ioc a b ↔ a < x ∧ x ≤ b := Iff.rfl

Membership Criterion for Left-Open Right-Closed Interval: $x \in (a, b] \leftrightarrow a < x \leq b$

Informal description

For any elements $a$, $b$, and $x$ in a preorder $\alpha$, the element $x$ belongs to the left-open right-closed interval $\text{Ioc}(a, b)$ if and only if $a < x$ and $x \leq b$.

Set.Ioc_def theorem

(a b : α) : {x | a < x ∧ x ≤ b} = Ioc a b

Full source

theorem Ioc_def (a b : α) : { x | a < x ∧ x ≤ b } = Ioc a b := rfl

Definition of Left-Open Right-Closed Interval via Set Builder Notation

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the set $\{x \mid a < x \wedge x \leq b\}$ is equal to the left-open right-closed interval $\text{Ioc}(a, b)$.

Set.Ici definition

(a : α)

Full source

/-- `Ici a` is the left-closed right-infinite interval $[a, ∞)$. -/
def Ici (a : α) := { x | a ≤ x }

Left-closed right-infinite interval

Informal description

The set `Ici a` is defined as the left-closed right-infinite interval $[a, \infty)$, consisting of all elements $x$ in the preorder $\alpha$ such that $a \leq x$.

Set.mem_Ici theorem

: x ∈ Ici a ↔ a ≤ x

Full source

@[simp] theorem mem_Ici : x ∈ Ici ax ∈ Ici a ↔ a ≤ x := Iff.rfl

Membership in $[a, \infty)$ is equivalent to $a \leq x$

Informal description

An element $x$ belongs to the left-closed right-infinite interval $[a, \infty)$ if and only if $a \leq x$.

Set.Ici_def theorem

(a : α) : {x | a ≤ x} = Ici a

Full source

theorem Ici_def (a : α) : { x | a ≤ x } = Ici a := rfl

Characterization of the Left-Closed Right-Infinite Interval as an Upper Set

Informal description

For any element $a$ in a preorder $\alpha$, the set $\{x \mid a \leq x\}$ is equal to the left-closed right-infinite interval $[a, \infty)$ (denoted as `Ici a`).

Set.Ioi definition

(a : α)

Full source

/-- `Ioi a` is the left-open right-infinite interval $(a, ∞)$. -/
def Ioi (a : α) := { x | a < x }

Left-open right-infinite interval

Informal description

For an element $ a $ in a preorder $ \alpha $, the set $ \text{Ioi}(a) $ is defined as the left-open right-infinite interval $ (a, \infty) $, consisting of all elements $ x $ in $ \alpha $ such that $ a < x $.

Set.mem_Ioi theorem

: x ∈ Ioi a ↔ a < x

Full source

@[simp] theorem mem_Ioi : x ∈ Ioi ax ∈ Ioi a ↔ a < x := Iff.rfl

Membership Criterion for Left-Open Right-Infinite Interval: $x \in (a, \infty) \leftrightarrow a < x$

Informal description

For any element $x$ in a preorder $\alpha$, $x$ belongs to the left-open right-infinite interval $(a, \infty)$ if and only if $a < x$.

Set.Ioi_def theorem

(a : α) : {x | a < x} = Ioi a

Full source

theorem Ioi_def (a : α) : { x | a < x } = Ioi a := rfl

Definition of $\text{Ioi}(a)$ as $\{x \mid a < x\}$

Informal description

For any element $a$ in a preorder $\alpha$, the set $\{x \mid a < x\}$ is equal to the left-open right-infinite interval $\text{Ioi}(a)$.

Set.OrdConnected structure

(s : Set α)

Full source

/-- 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`. -/
class OrdConnected (s : Set α) : Prop where
  /-- `s : Set α` is `OrdConnected` if for all `x y ∈ s` it includes the interval `[[x, y]]`. -/
  out' ⦃x : α⦄ (hx : x ∈ s) ⦃y : α⦄ (hy : y ∈ s) : IccIcc x y ⊆ s

Order Connected Set

Informal description

A set $s$ in a preorder $\alpha$ is called *order connected* if for any two elements $x, y \in s$, the closed interval $[x, y]$ is entirely contained in $s$. In a densely ordered conditionally complete linear order with the order topology, this condition is equivalent to $s$ being preconnected. For a linear ordered field, it is also equivalent to $s$ being convex.