Mathlib.Order.Interval.Set.Basic

Set.decidableMemIoo instance

[Decidable (a < x ∧ x < b)] : Decidable (x ∈ Ioo a b)

Full source

instance decidableMemIoo [Decidable (a < x ∧ x < b)] : Decidable (x ∈ Ioo a b) := by assumption

Decidability of Membership in Open Intervals

Informal description

For any elements $a$, $b$, and $x$ in a preorder $\alpha$, if the conjunction $a < x \land x < b$ is decidable, then membership in the open interval $(a, b)$ is decidable for $x$.

Set.decidableMemIco instance

[Decidable (a ≤ x ∧ x < b)] : Decidable (x ∈ Ico a b)

Full source

instance decidableMemIco [Decidable (a ≤ x ∧ x < b)] : Decidable (x ∈ Ico a b) := by assumption

Decidability of Membership in Left-Closed Right-Open Intervals

Informal description

For any elements $a$, $b$, and $x$ in a preorder $\alpha$, if the conjunction $a \leq x \wedge x < b$ is decidable, then membership $x \in \text{Ico}(a, b)$ is decidable.

Set.decidableMemIio instance

[Decidable (x < b)] : Decidable (x ∈ Iio b)

Full source

instance decidableMemIio [Decidable (x < b)] : Decidable (x ∈ Iio b) := by assumption

Decidability of Membership in Left-Infinite Right-Open Interval

Informal description

For any element $b$ in a preorder $\alpha$ and any element $x \in \alpha$, the proposition $x \in (-\infty, b)$ is decidable if the proposition $x < b$ is decidable.

Set.decidableMemIcc instance

[Decidable (a ≤ x ∧ x ≤ b)] : Decidable (x ∈ Icc a b)

Full source

instance decidableMemIcc [Decidable (a ≤ x ∧ x ≤ b)] : Decidable (x ∈ Icc a b) := by assumption

Decidability of Membership in Closed Intervals

Informal description

For any elements $ a $ and $ b $ in a preorder $ \alpha $ and any element $ x $, if the conjunction $ a \leq x \wedge x \leq b $ is decidable, then membership $ x \in [a, b] $ is decidable.

Set.decidableMemIic instance

[Decidable (x ≤ b)] : Decidable (x ∈ Iic b)

Full source

instance decidableMemIic [Decidable (x ≤ b)] : Decidable (x ∈ Iic b) := by assumption

Decidability of Membership in Left-Infinite Right-Closed Intervals

Informal description

For any element $x$ in a preorder $\alpha$ and any element $b$ in $\alpha$, if the inequality $x \leq b$ is decidable, then membership in the interval $(-\infty, b]$ is decidable.

Set.decidableMemIoc instance

[Decidable (a < x ∧ x ≤ b)] : Decidable (x ∈ Ioc a b)

Full source

instance decidableMemIoc [Decidable (a < x ∧ x ≤ b)] : Decidable (x ∈ Ioc a b) := by assumption

Decidability of Membership in Left-Open Right-Closed Intervals

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ and any element $x$ in $\alpha$, if the proposition $a < x \wedge x \leq b$ is decidable, then membership in the interval $\text{Ioc}(a, b)$ is decidable for $x$.

Set.decidableMemIci instance

[Decidable (a ≤ x)] : Decidable (x ∈ Ici a)

Full source

instance decidableMemIci [Decidable (a ≤ x)] : Decidable (x ∈ Ici a) := by assumption

Decidability of Membership in Left-Closed Right-Infinite Intervals

Informal description

For any preorder $\alpha$ and elements $a, x \in \alpha$, if there is a decidable procedure for determining whether $a \leq x$, then membership in the interval $[a, \infty)$ is also decidable.

Set.decidableMemIoi instance

[Decidable (a < x)] : Decidable (x ∈ Ioi a)

Full source

instance decidableMemIoi [Decidable (a < x)] : Decidable (x ∈ Ioi a) := by assumption

Decidability of Membership in Left-Open Right-Infinite Intervals

Informal description

For any preorder $\alpha$ and elements $a, x \in \alpha$, if the proposition $a < x$ is decidable, then the membership $x \in \text{Ioi}(a)$ is also decidable.

Set.left_mem_Ioo theorem

: a ∈ Ioo a b ↔ False

Full source

theorem left_mem_Ioo : a ∈ Ioo a ba ∈ Ioo a b ↔ False := by simp [lt_irrefl]

Non-membership of Left Endpoint in Open Interval

Informal description

For any elements $a$ and $b$ in a preorder, the element $a$ does not belong to the open interval $(a, b)$. In other words, $a \in (a, b) \leftrightarrow \text{False}$.

Set.left_mem_Ico theorem

: a ∈ Ico a b ↔ a < b

Full source

theorem left_mem_Ico : a ∈ Ico a ba ∈ Ico a b ↔ a < b := by simp [le_refl]

Membership of Left Endpoint in Left-Closed Right-Open Interval: $a \in [a, b) \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a preorder, the element $a$ belongs to the left-closed right-open interval $[a, b)$ if and only if $a < b$.

Set.left_mem_Icc theorem

: a ∈ Icc a b ↔ a ≤ b

Full source

theorem left_mem_Icc : a ∈ Icc a ba ∈ Icc a b ↔ a ≤ b := by simp [le_refl]

Membership of Left Endpoint in Closed Interval: $a \in [a, b] \leftrightarrow a \leq b$

Informal description

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

Set.left_mem_Ioc theorem

: a ∈ Ioc a b ↔ False

Full source

theorem left_mem_Ioc : a ∈ Ioc a ba ∈ Ioc a b ↔ False := by simp [lt_irrefl]

Non-membership of Left Endpoint in Left-Open Right-Closed Interval

Informal description

For any elements $a$ and $b$ in a preorder, the left endpoint $a$ does not belong to the left-open right-closed interval $(a, b]$. In other words, $a \notin (a, b]$.

Set.left_mem_Ici theorem

: a ∈ Ici a

Full source

theorem left_mem_Ici : a ∈ Ici a := by simp

Element Belongs to Its Own Left-Closed Right-Infinite Interval

Informal description

For any element $a$ in a preorder $\alpha$, $a$ belongs to the left-closed right-infinite interval $[a, \infty)$, i.e., $a \in [a, \infty)$.

Set.right_mem_Ioo theorem

: b ∈ Ioo a b ↔ False

Full source

theorem right_mem_Ioo : b ∈ Ioo a bb ∈ Ioo a b ↔ False := by simp [lt_irrefl]

Non-membership of Right Endpoint in Open Interval $(a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the right endpoint $b$ does not belong to the open interval $(a, b)$, i.e., $b \notin (a, b)$.

Set.right_mem_Ico theorem

: b ∈ Ico a b ↔ False

Full source

theorem right_mem_Ico : b ∈ Ico a bb ∈ Ico a b ↔ False := by simp [lt_irrefl]

Non-membership of Right Endpoint in Left-Closed Right-Open Interval

Informal description

For any elements $a$ and $b$ in a preorder, the right endpoint $b$ is not in the left-closed right-open interval $\text{Ico}(a, b)$, i.e., $b \notin [a, b)$.

Set.right_mem_Icc theorem

: b ∈ Icc a b ↔ a ≤ b

Full source

theorem right_mem_Icc : b ∈ Icc a bb ∈ Icc a b ↔ a ≤ b := by simp [le_refl]

Membership of Right Endpoint in Closed Interval: $b \in [a, b] \leftrightarrow a \leq b$

Informal description

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

Set.right_mem_Ioc theorem

: b ∈ Ioc a b ↔ a < b

Full source

theorem right_mem_Ioc : b ∈ Ioc a bb ∈ Ioc a b ↔ a < b := by simp [le_refl]

Membership of Right Endpoint in Left-Open Right-Closed Interval: $b \in (a, b] \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a preorder, the element $b$ belongs to the left-open right-closed interval $(a, b]$ if and only if $a < b$.

Set.right_mem_Iic theorem

: a ∈ Iic a

Full source

theorem right_mem_Iic : a ∈ Iic a := by simp

Element is in its own right-closed interval

Informal description

For any element $a$ in a preorder, $a$ belongs to the left-infinite right-closed interval $(-\infty, a]$, i.e., $a \in (-\infty, a]$.

Set.Ici_toDual theorem

: Ici (toDual a) = ofDual ⁻¹' Iic a

Full source

@[simp]
theorem Ici_toDual : Ici (toDual a) = ofDualofDual ⁻¹' Iic a :=
  rfl

Duality between $\operatorname{Ici}$ and $\operatorname{Iic}$ via order reversal

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-infinite interval $[\operatorname{toDual}(a), \infty)$ in the order dual of $\alpha$ is equal to the preimage under the order-reversing map $\operatorname{ofDual}$ of the left-infinite right-closed interval $(-\infty, a]$ in $\alpha$, i.e., $$ \operatorname{Ici}(\operatorname{toDual}(a)) = \operatorname{ofDual}^{-1}(\operatorname{Iic}(a)). $$

Set.Iic_toDual theorem

: Iic (toDual a) = ofDual ⁻¹' Ici a

Full source

@[simp]
theorem Iic_toDual : Iic (toDual a) = ofDualofDual ⁻¹' Ici a :=
  rfl

Duality between $\operatorname{Iic}$ and $\operatorname{Ici}$ via order reversal

Informal description

For any element $a$ in a preorder $\alpha$, the left-infinite right-closed interval $(-\infty, \operatorname{toDual}(a)]$ in the order dual of $\alpha$ is equal to the preimage under the order-reversing map $\operatorname{ofDual}$ of the left-closed right-infinite interval $[a, \infty)$ in $\alpha$, i.e., $$ \operatorname{Iic}(\operatorname{toDual}(a)) = \operatorname{ofDual}^{-1}(\operatorname{Ici}(a)). $$

Set.Ioi_toDual theorem

: Ioi (toDual a) = ofDual ⁻¹' Iio a

Full source

@[simp]
theorem Ioi_toDual : Ioi (toDual a) = ofDualofDual ⁻¹' Iio a :=
  rfl

Duality between $\operatorname{Ioi}$ and $\operatorname{Iio}$ via order reversal

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-infinite interval $(a^\ast, \infty)$ in the order dual of $\alpha$ is equal to the preimage under the order-reversing map $\operatorname{ofDual}$ of the left-infinite right-open interval $(-\infty, a)$ in $\alpha$, i.e., $$ \operatorname{Ioi}(\operatorname{toDual}(a)) = \operatorname{ofDual}^{-1}(\operatorname{Iio}(a)). $$

Set.Iio_toDual theorem

: Iio (toDual a) = ofDual ⁻¹' Ioi a

Full source

@[simp]
theorem Iio_toDual : Iio (toDual a) = ofDualofDual ⁻¹' Ioi a :=
  rfl

Duality between $\operatorname{Iio}$ and $\operatorname{Ioi}$ via order reversal

Informal description

For any element $a$ in a preorder $\alpha$, the left-infinite right-open interval $(-\infty, a^\ast)$ in the order dual of $\alpha$ is equal to the preimage under the order-reversing map $\operatorname{ofDual}$ of the left-open right-infinite interval $(a, \infty)$ in $\alpha$, i.e., $$ \operatorname{Iio}(\operatorname{toDual}(a)) = \operatorname{ofDual}^{-1}(\operatorname{Ioi}(a)). $$

Set.Icc_toDual theorem

: Icc (toDual a) (toDual b) = ofDual ⁻¹' Icc b a

Full source

@[simp]
theorem Icc_toDual : Icc (toDual a) (toDual b) = ofDualofDual ⁻¹' Icc b a :=
  Set.ext fun _ => and_comm

Duality between closed intervals via order reversal

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the closed interval $[a^\ast, b^\ast]$ in the order dual of $\alpha$ is equal to the preimage under the order-reversing map $\operatorname{ofDual}$ of the closed interval $[b, a]$ in $\alpha$, i.e., $$ \operatorname{Icc}(\operatorname{toDual}(a), \operatorname{toDual}(b)) = \operatorname{ofDual}^{-1}(\operatorname{Icc}(b, a)). $$

Set.Ioc_toDual theorem

: Ioc (toDual a) (toDual b) = ofDual ⁻¹' Ico b a

Full source

@[simp]
theorem Ioc_toDual : Ioc (toDual a) (toDual b) = ofDualofDual ⁻¹' Ico b a :=
  Set.ext fun _ => and_comm

Duality between $\operatorname{Ioc}$ and $\operatorname{Ico}$ via order reversal

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-open right-closed interval $(\text{toDual}(a), \text{toDual}(b)]$ in the order dual $\alpha^{\text{op}}$ is equal to the preimage under $\text{ofDual}$ of the left-closed right-open interval $[b, a)$ in $\alpha$. In other words: $$(\text{toDual}(a), \text{toDual}(b)] = \text{ofDual}^{-1}\big([b, a)\big)$$

Set.Ico_toDual theorem

: Ico (toDual a) (toDual b) = ofDual ⁻¹' Ioc b a

Full source

@[simp]
theorem Ico_toDual : Ico (toDual a) (toDual b) = ofDualofDual ⁻¹' Ioc b a :=
  Set.ext fun _ => and_comm

Duality between $\operatorname{Ico}$ and $\operatorname{Ioc}$ via order reversal

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-closed right-open interval $[\operatorname{toDual}(a), \operatorname{toDual}(b))$ in the order dual of $\alpha$ is equal to the preimage under the order-reversing map $\operatorname{ofDual}$ of the left-open right-closed interval $(b, a]$ in $\alpha$, i.e., $$ \operatorname{Ico}(\operatorname{toDual}(a), \operatorname{toDual}(b)) = \operatorname{ofDual}^{-1}(\operatorname{Ioc}(b, a)). $$

Set.Ioo_toDual theorem

: Ioo (toDual a) (toDual b) = ofDual ⁻¹' Ioo b a

Full source

@[simp]
theorem Ioo_toDual : Ioo (toDual a) (toDual b) = ofDualofDual ⁻¹' Ioo b a :=
  Set.ext fun _ => and_comm

Duality between open intervals in order duals: $(\text{toDual}(a), \text{toDual}(b)) = \text{ofDual}^{-1}((b, a))$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the open interval $(\text{toDual}(a), \text{toDual}(b))$ in the order dual $\alpha^{\text{op}}$ is equal to the preimage under $\text{ofDual}$ of the open interval $(b, a)$ in $\alpha$. In other words: $$(\text{toDual}(a), \text{toDual}(b)) = \text{ofDual}^{-1}\big((b, a)\big)$$

Set.Ici_ofDual theorem

{x : αᵒᵈ} : Ici (ofDual x) = toDual ⁻¹' Iic x

Full source

@[simp]
theorem Ici_ofDual {x : αᵒᵈ} : Ici (ofDual x) = toDualtoDual ⁻¹' Iic x :=
  rfl

Duality between $[\text{ofDual}(x), \infty)$ and $(-\infty, x]$ in order duals

Informal description

For any element $x$ in the order dual of a preorder $\alpha$ (denoted $\alpha^{\text{op}}$), the left-closed right-infinite interval $[\text{ofDual}(x), \infty)$ in $\alpha$ is equal to the preimage under $\text{toDual}$ of the left-infinite right-closed interval $(-\infty, x]$ in $\alpha^{\text{op}}$. In other words: $$[\text{ofDual}(x), \infty) = \text{toDual}^{-1}\big((-\infty, x]\big)$$

Set.Iic_ofDual theorem

{x : αᵒᵈ} : Iic (ofDual x) = toDual ⁻¹' Ici x

Full source

@[simp]
theorem Iic_ofDual {x : αᵒᵈ} : Iic (ofDual x) = toDualtoDual ⁻¹' Ici x :=
  rfl

Dual Interval Correspondence: $\text{Iic}$ in Original Order Equals Preimage of $\text{Ici}$ in Dual Order

Informal description

For any element $x$ in the order dual $\alpha^\text{op}$ of a preorder $\alpha$, the left-infinite right-closed interval $(-\infty, \text{ofDual}(x)]$ in $\alpha$ is equal to the preimage under $\text{toDual}$ of the left-closed right-infinite interval $[x, \infty)$ in $\alpha^\text{op}$. In other words: $$(-\infty, \text{ofDual}(x)]_\alpha = \text{toDual}^{-1}\big([x, \infty)_{\alpha^\text{op}}\big)$$

Set.Ioi_ofDual theorem

{x : αᵒᵈ} : Ioi (ofDual x) = toDual ⁻¹' Iio x

Full source

@[simp]
theorem Ioi_ofDual {x : αᵒᵈ} : Ioi (ofDual x) = toDualtoDual ⁻¹' Iio x :=
  rfl

Dual Order Correspondence: $\text{Ioi}$ in Dual Equals Preimage of $\text{Iio}$

Informal description

For any element $x$ in the order dual $\alpha^\text{op}$ of a preorder $\alpha$, the left-open right-infinite interval $(\text{ofDual}(x), \infty)$ in the dual order is equal to the preimage under $\text{toDual}$ of the left-infinite right-open interval $(-\infty, x)$ in the original order. In other words: $$(\text{ofDual}(x), \infty)_{\alpha^\text{op}} = \text{toDual}^{-1}\big((-\infty, x)_\alpha\big)$$

Set.Iio_ofDual theorem

{x : αᵒᵈ} : Iio (ofDual x) = toDual ⁻¹' Ioi x

Full source

@[simp]
theorem Iio_ofDual {x : αᵒᵈ} : Iio (ofDual x) = toDualtoDual ⁻¹' Ioi x :=
  rfl

Dual Interval Correspondence: $\text{Iio}$ in Dual Order Equals Preimage of $\text{Ioi}$

Informal description

For any element $x$ in the order dual $\alpha^\text{op}$ of a preorder $\alpha$, the left-infinite right-open interval $\text{Iio}(\text{ofDual}(x))$ is equal to the preimage under $\text{toDual}$ of the left-open right-infinite interval $\text{Ioi}(x)$. In other words: \[ (-\infty, x)_{\alpha^\text{op}} = \text{toDual}^{-1}\big((x, \infty)_\alpha\big) \] where $(-\infty, x)_{\alpha^\text{op}}$ denotes the interval in the dual order and $(x, \infty)_\alpha$ denotes the interval in the original order.

Set.Icc_ofDual theorem

{x y : αᵒᵈ} : Icc (ofDual y) (ofDual x) = toDual ⁻¹' Icc x y

Full source

@[simp]
theorem Icc_ofDual {x y : αᵒᵈ} : Icc (ofDual y) (ofDual x) = toDualtoDual ⁻¹' Icc x y :=
  Set.ext fun _ => and_comm

Dual Interval Correspondence: Closed Interval in Dual Order Equals Preimage of Closed Interval

Informal description

For any elements $x$ and $y$ in the order dual $\alpha^\text{op}$ of a preorder $\alpha$, the closed interval $[\text{ofDual}(y), \text{ofDual}(x)]$ in the dual order is equal to the preimage under $\text{toDual}$ of the closed interval $[x, y]$ in the original order. In other words: \[ [y, x]_{\alpha^\text{op}} = \text{toDual}^{-1}\big([x, y]_\alpha\big) \] where $[y, x]_{\alpha^\text{op}}$ denotes the interval in the dual order and $[x, y]_\alpha$ denotes the interval in the original order.

Set.Ico_ofDual theorem

{x y : αᵒᵈ} : Ico (ofDual y) (ofDual x) = toDual ⁻¹' Ioc x y

Full source

@[simp]
theorem Ico_ofDual {x y : αᵒᵈ} : Ico (ofDual y) (ofDual x) = toDualtoDual ⁻¹' Ioc x y :=
  Set.ext fun _ => and_comm

Dual Interval Correspondence: $\text{Ico}$ in Dual Order Equals Preimage of $\text{Ioc}$

Informal description

For any elements $x$ and $y$ in the order dual $\alpha^\text{op}$ of a preorder $\alpha$, the left-closed right-open interval $\text{Ico}(\text{ofDual}(y), \text{ofDual}(x))$ is equal to the preimage under $\text{toDual}$ of the left-open right-closed interval $\text{Ioc}(x, y)$. In other words: \[ [y, x)_{\alpha^\text{op}} = \text{toDual}^{-1}\big((x, y]_\alpha\big) \] where $[y, x)_{\alpha^\text{op}}$ denotes the interval in the dual order and $(x, y]_\alpha$ denotes the interval in the original order.

Set.Ioc_ofDual theorem

{x y : αᵒᵈ} : Ioc (ofDual y) (ofDual x) = toDual ⁻¹' Ico x y

Full source

@[simp]
theorem Ioc_ofDual {x y : αᵒᵈ} : Ioc (ofDual y) (ofDual x) = toDualtoDual ⁻¹' Ico x y :=
  Set.ext fun _ => and_comm

Dual Interval Correspondence: $\text{Ioc}$ in Dual Order Equals Preimage of $\text{Ico}$

Informal description

For any elements $x$ and $y$ in the order dual $\alpha^\text{op}$ of a preorder $\alpha$, the left-open right-closed interval $\text{Ioc}(\text{ofDual}(y), \text{ofDual}(x))$ is equal to the preimage under $\text{toDual}$ of the left-closed right-open interval $\text{Ico}(x, y)$. In other words: \[ (y, x]_{\alpha^\text{op}} = \text{toDual}^{-1}\big([x, y)_\alpha\big) \] where $(y, x]_{\alpha^\text{op}}$ denotes the interval in the dual order and $[x, y)_\alpha$ denotes the interval in the original order.

Set.Ioo_ofDual theorem

{x y : αᵒᵈ} : Ioo (ofDual y) (ofDual x) = toDual ⁻¹' Ioo x y

Full source

@[simp]
theorem Ioo_ofDual {x y : αᵒᵈ} : Ioo (ofDual y) (ofDual x) = toDualtoDual ⁻¹' Ioo x y :=
  Set.ext fun _ => and_comm

Dual Open Interval Correspondence: $\text{Ioo}$ in Dual Order Equals Preimage of $\text{Ioo}$

Informal description

For any elements $x$ and $y$ in the order dual $\alpha^\text{op}$ of a preorder $\alpha$, the open interval $\text{Ioo}(\text{ofDual}(y), \text{ofDual}(x))$ is equal to the preimage under $\text{toDual}$ of the open interval $\text{Ioo}(x, y)$. In other words: \[ (y, x)_{\alpha^\text{op}} = \text{toDual}^{-1}\big((x, y)_\alpha\big) \] where $(y, x)_{\alpha^\text{op}}$ denotes the interval in the dual order and $(x, y)_\alpha$ denotes the interval in the original order.

Set.nonempty_Icc theorem

: (Icc a b).Nonempty ↔ a ≤ b

Full source

@[simp]
theorem nonempty_Icc : (Icc a b).Nonempty ↔ a ≤ b :=
  ⟨fun ⟨_, hx⟩ => hx.1.trans hx.2, fun h => ⟨a, left_mem_Icc.2 h⟩⟩

Nonemptiness of Closed Interval Equivalent to $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder, the closed interval $[a, b]$ is nonempty if and only if $a \leq b$.

Set.nonempty_Ico theorem

: (Ico a b).Nonempty ↔ a < b

Full source

@[simp]
theorem nonempty_Ico : (Ico a b).Nonempty ↔ a < b :=
  ⟨fun ⟨_, hx⟩ => hx.1.trans_lt hx.2, fun h => ⟨a, left_mem_Ico.2 h⟩⟩

Nonemptiness of $[a, b)$ Interval Equivalent to $a < b$

Informal description

For any elements $a$ and $b$ in a preorder, the left-closed right-open interval $[a, b)$ is nonempty if and only if $a < b$.

Set.nonempty_Ioc theorem

: (Ioc a b).Nonempty ↔ a < b

Full source

@[simp]
theorem nonempty_Ioc : (Ioc a b).Nonempty ↔ a < b :=
  ⟨fun ⟨_, hx⟩ => hx.1.trans_le hx.2, fun h => ⟨b, right_mem_Ioc.2 h⟩⟩

Nonemptiness of $(a, b]$ Interval Equivalent to $a < b$

Informal description

For any elements $a$ and $b$ in a preorder, the left-open right-closed interval $(a, b]$ is nonempty if and only if $a < b$.

Set.nonempty_Ici theorem

: (Ici a).Nonempty

Full source

@[simp]
theorem nonempty_Ici : (Ici a).Nonempty :=
  ⟨a, left_mem_Ici⟩

Nonemptiness of $[a, \infty)$ Interval

Informal description

For any element $a$ in a preorder, the left-closed right-infinite interval $[a, \infty)$ is nonempty.

Set.nonempty_Iic theorem

: (Iic a).Nonempty

Full source

@[simp]
theorem nonempty_Iic : (Iic a).Nonempty :=
  ⟨a, right_mem_Iic⟩

Nonemptiness of Left-Infinite Right-Closed Interval

Informal description

For any element $a$ in a preorder, the left-infinite right-closed interval $(-\infty, a]$ is nonempty.

Set.nonempty_Ioo theorem

[DenselyOrdered α] : (Ioo a b).Nonempty ↔ a < b

Full source

@[simp]
theorem nonempty_Ioo [DenselyOrdered α] : (Ioo a b).Nonempty ↔ a < b :=
  ⟨fun ⟨_, ha, hb⟩ => ha.trans hb, exists_between⟩

Nonempty Open Interval Condition in Densely Ordered Sets

Informal description

In a densely ordered set $\alpha$, the open interval $(a, b)$ is nonempty if and only if $a < b$.

Set.nonempty_Ioi theorem

[NoMaxOrder α] : (Ioi a).Nonempty

Full source

@[simp]
theorem nonempty_Ioi [NoMaxOrder α] : (Ioi a).Nonempty :=
  exists_gt a

Nonemptiness of Right-Infinite Open Interval in NoMaxOrder

Informal description

In a preorder $\alpha$ with no maximal element (i.e., for every $a \in \alpha$ there exists $b \in \alpha$ such that $a < b$), the left-open right-infinite interval $(a, \infty)$ is nonempty for any $a \in \alpha$.

Set.nonempty_Iio theorem

[NoMinOrder α] : (Iio a).Nonempty

Full source

@[simp]
theorem nonempty_Iio [NoMinOrder α] : (Iio a).Nonempty :=
  exists_lt a

Nonemptiness of Left-Infinite Right-Open Interval in No-Min-Order Preorder

Informal description

In a preorder $\alpha$ with no minimal element (i.e., for every $a \in \alpha$, there exists $x \in \alpha$ such that $x < a$), the left-infinite right-open interval $(-\infty, a)$ is nonempty.

Set.nonempty_Icc_subtype theorem

(h : a ≤ b) : Nonempty (Icc a b)

Full source

theorem nonempty_Icc_subtype (h : a ≤ b) : Nonempty (Icc a b) :=
  Nonempty.to_subtype (nonempty_Icc.mpr h)

Nonemptiness of Closed Interval Subtype Given $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the closed interval $[a, b]$ is nonempty as a subtype.

Set.nonempty_Ico_subtype theorem

(h : a < b) : Nonempty (Ico a b)

Full source

theorem nonempty_Ico_subtype (h : a < b) : Nonempty (Ico a b) :=
  Nonempty.to_subtype (nonempty_Ico.mpr h)

Nonemptiness of $[a, b)$ Interval Given $a < b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a < b$, the left-closed right-open interval $[a, b)$ is nonempty.

Set.nonempty_Ioc_subtype theorem

(h : a < b) : Nonempty (Ioc a b)

Full source

theorem nonempty_Ioc_subtype (h : a < b) : Nonempty (Ioc a b) :=
  Nonempty.to_subtype (nonempty_Ioc.mpr h)

Nonemptiness of $(a, b]$ Interval Subtype Given $a < b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a < b$, the left-open right-closed interval $(a, b]$ is nonempty as a subtype.

Set.nonempty_Ici_subtype instance

: Nonempty (Ici a)

Full source

/-- An interval `Ici a` is nonempty. -/
instance nonempty_Ici_subtype : Nonempty (Ici a) :=
  Nonempty.to_subtype nonempty_Ici

Nonemptiness of $[a, \infty)$ Interval

Informal description

For any element $a$ in a preorder, the left-closed right-infinite interval $[a, \infty)$ is nonempty.

Set.nonempty_Iic_subtype instance

: Nonempty (Iic a)

Full source

/-- An interval `Iic a` is nonempty. -/
instance nonempty_Iic_subtype : Nonempty (Iic a) :=
  Nonempty.to_subtype nonempty_Iic

Nonemptiness of Left-Infinite Right-Closed Interval

Informal description

For any element $a$ in a preorder, the left-infinite right-closed interval $(-\infty, a]$ is nonempty.

Set.nonempty_Ioo_subtype theorem

[DenselyOrdered α] (h : a < b) : Nonempty (Ioo a b)

Full source

theorem nonempty_Ioo_subtype [DenselyOrdered α] (h : a < b) : Nonempty (Ioo a b) :=
  Nonempty.to_subtype (nonempty_Ioo.mpr h)

Nonemptiness of Open Interval in Densely Ordered Sets

Informal description

In a densely ordered set $\alpha$, if $a < b$, then the open interval $(a, b)$ is nonempty.

Set.nonempty_Ioi_subtype instance

[NoMaxOrder α] : Nonempty (Ioi a)

Full source

/-- In an order without maximal elements, the intervals `Ioi` are nonempty. -/
instance nonempty_Ioi_subtype [NoMaxOrder α] : Nonempty (Ioi a) :=
  Nonempty.to_subtype nonempty_Ioi

Nonemptiness of Right-Infinite Open Interval in Orders Without Maximal Elements

Informal description

For any preorder $\alpha$ with no maximal element and any element $a \in \alpha$, the left-open right-infinite interval $(a, \infty)$ is nonempty.

Set.nonempty_Iio_subtype instance

[NoMinOrder α] : Nonempty (Iio a)

Full source

/-- In an order without minimal elements, the intervals `Iio` are nonempty. -/
instance nonempty_Iio_subtype [NoMinOrder α] : Nonempty (Iio a) :=
  Nonempty.to_subtype nonempty_Iio

Nonemptiness of Left-Infinite Right-Open Interval in Orders Without Minimal Elements

Informal description

In a preorder $\alpha$ with no minimal element, the left-infinite right-open interval $(-\infty, a)$ is nonempty.

Set.instNoMinOrderElemIio instance

[NoMinOrder α] : NoMinOrder (Iio a)

Full source

instance [NoMinOrder α] : NoMinOrder (Iio a) :=
  ⟨fun a =>
    let ⟨b, hb⟩ := exists_lt (a : α)
    ⟨⟨b, lt_trans hb a.2⟩, hb⟩⟩

No Minimal Element in Left-Infinite Right-Open Interval

Informal description

For any preorder $\alpha$ with no minimal element, the left-infinite right-open interval $(-\infty, a)$ also has no minimal element.

Set.instNoMinOrderElemIic instance

[NoMinOrder α] : NoMinOrder (Iic a)

Full source

instance [NoMinOrder α] : NoMinOrder (Iic a) :=
  ⟨fun a =>
    let ⟨b, hb⟩ := exists_lt (a : α)
    ⟨⟨b, hb.le.trans a.2⟩, hb⟩⟩

No Minimal Element in $(-\infty, a]$ for NoMinOrder $\alpha$

Informal description

For any preorder $\alpha$ with no minimal element, the left-infinite right-closed interval $(-\infty, a]$ also has no minimal element.

Set.instNoMaxOrderElemIoi instance

[NoMaxOrder α] : NoMaxOrder (Ioi a)

Full source

instance [NoMaxOrder α] : NoMaxOrder (Ioi a) :=
  OrderDual.noMaxOrder (α := Iio (toDual a))

No Maximal Element in Left-Open Right-Infinite Interval

Informal description

For any preorder $\alpha$ with no maximal element, the left-open right-infinite interval $(a, \infty)$ also has no maximal element.

Set.instNoMaxOrderElemIci instance

[NoMaxOrder α] : NoMaxOrder (Ici a)

Full source

instance [NoMaxOrder α] : NoMaxOrder (Ici a) :=
  OrderDual.noMaxOrder (α := Iic (toDual a))

No Maximal Element in $[a, \infty)$ for NoMaxOrder $\alpha$

Informal description

For any preorder $\alpha$ with no maximal element, the left-closed right-infinite interval $[a, \infty)$ also has no maximal element.

Set.Icc_eq_empty theorem

(h : ¬a ≤ b) : Icc a b = ∅

Full source

@[simp]
theorem Icc_eq_empty (h : ¬a ≤ b) : Icc a b = ∅ :=
  eq_empty_iff_forall_not_mem.2 fun _ ⟨ha, hb⟩ => h (ha.trans hb)

Empty Closed Interval When Not $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder, if $a \not\leq b$, then the closed interval $[a, b]$ is empty.

Set.Ico_eq_empty theorem

(h : ¬a < b) : Ico a b = ∅

Full source

@[simp]
theorem Ico_eq_empty (h : ¬a < b) : Ico a b = ∅ :=
  eq_empty_iff_forall_not_mem.2 fun _ ⟨ha, hb⟩ => h (ha.trans_lt hb)

Empty Left-Closed Right-Open Interval When Not Strictly Increasing

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, if $a$ is not less than $b$ (i.e., $\neg (a < b)$), then the left-closed right-open interval $\text{Ico}(a, b)$ is empty.

Set.Ioc_eq_empty theorem

(h : ¬a < b) : Ioc a b = ∅

Full source

@[simp]
theorem Ioc_eq_empty (h : ¬a < b) : Ioc a b = ∅ :=
  eq_empty_iff_forall_not_mem.2 fun _ ⟨ha, hb⟩ => h (ha.trans_le hb)

Empty Left-Open Right-Closed Interval When Not Strictly Increasing

Informal description

For any two elements $a$ and $b$ in a preorder, if $a$ is not less than $b$ (i.e., $\neg (a < b)$), then the left-open right-closed interval $(a, b]$ is empty.

Set.Ioo_eq_empty theorem

(h : ¬a < b) : Ioo a b = ∅

Full source

@[simp]
theorem Ioo_eq_empty (h : ¬a < b) : Ioo a b = ∅ :=
  eq_empty_iff_forall_not_mem.2 fun _ ⟨ha, hb⟩ => h (ha.trans hb)

Empty Open Interval When Not Strictly Increasing

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, if $a$ is not strictly less than $b$ (i.e., $\neg (a < b)$), then the open interval $(a, b)$ is empty.

Set.Icc_eq_empty_of_lt theorem

(h : b < a) : Icc a b = ∅

Full source

@[simp]
theorem Icc_eq_empty_of_lt (h : b < a) : Icc a b = ∅ :=
  Icc_eq_empty h.not_le

Empty Closed Interval When $b < a$

Informal description

For any elements $a$ and $b$ in a preorder, if $b < a$, then the closed interval $[a, b]$ is empty.

Set.Ico_eq_empty_of_le theorem

(h : b ≤ a) : Ico a b = ∅

Full source

@[simp]
theorem Ico_eq_empty_of_le (h : b ≤ a) : Ico a b = ∅ :=
  Ico_eq_empty h.not_lt

Empty Left-Closed Right-Open Interval When Non-Increasing

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, if $b \leq a$, then the left-closed right-open interval $\text{Ico}(a, b)$ is empty.

Set.Ioc_eq_empty_of_le theorem

(h : b ≤ a) : Ioc a b = ∅

Full source

@[simp]
theorem Ioc_eq_empty_of_le (h : b ≤ a) : Ioc a b = ∅ :=
  Ioc_eq_empty h.not_lt

Empty Left-Open Right-Closed Interval When Non-Increasing

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, if $b \leq a$, then the left-open right-closed interval $\text{Ioc}(a, b)$ is empty, i.e., $(a, b] = \emptyset$.

Set.Ioo_eq_empty_of_le theorem

(h : b ≤ a) : Ioo a b = ∅

Full source

@[simp]
theorem Ioo_eq_empty_of_le (h : b ≤ a) : Ioo a b = ∅ :=
  Ioo_eq_empty h.not_lt

Empty Open Interval When Non-Increasing

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, if $b \leq a$, then the open interval $(a, b)$ is empty, i.e., $\text{Ioo}(a, b) = \emptyset$.

Set.Ico_self theorem

(a : α) : Ico a a = ∅

Full source

theorem Ico_self (a : α) : Ico a a = ∅ :=
  Ico_eq_empty <| lt_irrefl _

Empty Interval Property: $\text{Ico}(a, a) = \emptyset$

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-open interval $\text{Ico}(a, a)$ is empty.

Set.Ioc_self theorem

(a : α) : Ioc a a = ∅

Full source

theorem Ioc_self (a : α) : Ioc a a = ∅ :=
  Ioc_eq_empty <| lt_irrefl _

Empty Left-Open Right-Closed Interval at a Point: $\text{Ioc}(a, a) = \emptyset$

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-closed interval $(a, a]$ is empty, i.e., $\text{Ioc}(a, a) = \emptyset$.

Set.Ioo_self theorem

(a : α) : Ioo a a = ∅

Full source

theorem Ioo_self (a : α) : Ioo a a = ∅ :=
  Ioo_eq_empty <| lt_irrefl _

Empty Open Interval at a Point: $\text{Ioo}(a, a) = \emptyset$

Informal description

For any element $a$ in a preorder $\alpha$, the open interval $(a, a)$ is empty, i.e., $\text{Ioo}(a, a) = \emptyset$.

Set.Ici_subset_Ici theorem

: Ici a ⊆ Ici b ↔ b ≤ a

Full source

@[simp]
theorem Ici_subset_Ici : IciIci a ⊆ Ici bIci a ⊆ Ici b ↔ b ≤ a :=
  ⟨fun h => h <| left_mem_Ici, fun h _ hx => h.trans hx⟩

Subset Condition for Left-Closed Right-Infinite Intervals: $[a, \infty) \subseteq [b, \infty) \leftrightarrow b \leq a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-closed right-infinite interval $[a, \infty)$ is a subset of $[b, \infty)$ if and only if $b \leq a$.

Set.Ici_ssubset_Ici theorem

: Ici a ⊂ Ici b ↔ b < a

Full source

@[simp]
theorem Ici_ssubset_Ici : IciIci a ⊂ Ici bIci a ⊂ Ici b ↔ b < a where
  mp h := by
    obtain ⟨ab, c, cb, ac⟩ := ssubset_iff_exists.mp h
    exact lt_of_le_not_le (Ici_subset_Ici.mp ab) (fun h' ↦ ac (h'.trans cb))
  mpr h := (ssubset_iff_of_subset (Ici_subset_Ici.mpr h.le)).mpr
    ⟨b, right_mem_Iic, fun h' => h.not_le h'⟩

Strict Subset Condition for Left-Closed Right-Infinite Intervals: $[a, \infty) \subset [b, \infty) \leftrightarrow b < a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-closed right-infinite interval $[a, \infty)$ is a strict subset of $[b, \infty)$ if and only if $b < a$.

Set.Iic_subset_Iic theorem

: Iic a ⊆ Iic b ↔ a ≤ b

Full source

@[simp]
theorem Iic_subset_Iic : IicIic a ⊆ Iic bIic a ⊆ Iic b ↔ a ≤ b :=
  @Ici_subset_Ici αᵒᵈ _ _ _

Subset Condition for Left-Infinite Right-Closed Intervals: $(-\infty, a] \subseteq (-\infty, b] \leftrightarrow a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-infinite right-closed interval $(-\infty, a]$ is a subset of $(-\infty, b]$ if and only if $a \leq b$.

Set.Iic_ssubset_Iic theorem

: Iic a ⊂ Iic b ↔ a < b

Full source

@[simp]
theorem Iic_ssubset_Iic : IicIic a ⊂ Iic bIic a ⊂ Iic b ↔ a < b :=
  @Ici_ssubset_Ici αᵒᵈ _ _ _

Strict Subset Condition for Left-Infinite Right-Closed Intervals: $(-\infty, a] \subset (-\infty, b] \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-infinite right-closed interval $(-\infty, a]$ is a strict subset of $(-\infty, b]$ if and only if $a < b$.

Set.Ici_subset_Ioi theorem

: Ici a ⊆ Ioi b ↔ b < a

Full source

@[simp]
theorem Ici_subset_Ioi : IciIci a ⊆ Ioi bIci a ⊆ Ioi b ↔ b < a :=
  ⟨fun h => h left_mem_Ici, fun h _ hx => h.trans_le hx⟩

Inclusion of Closed-Open Infinite Intervals: $[a, \infty) \subseteq (b, \infty) \leftrightarrow b < a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-closed right-infinite interval $[a, \infty)$ is a subset of the left-open right-infinite interval $(b, \infty)$ if and only if $b < a$.

Set.Iic_subset_Iio theorem

: Iic a ⊆ Iio b ↔ a < b

Full source

@[simp]
theorem Iic_subset_Iio : IicIic a ⊆ Iio bIic a ⊆ Iio b ↔ a < b :=
  ⟨fun h => h right_mem_Iic, fun h _ hx => lt_of_le_of_lt hx h⟩

Inclusion of Closed-Open Infinite Intervals: $(-\infty, a] \subseteq (-\infty, b) \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-infinite right-closed interval $(-\infty, a]$ is a subset of the left-infinite right-open interval $(-\infty, b)$ if and only if $a < b$.

Set.Ioo_subset_Ioo theorem

(h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : Ioo a₁ b₁ ⊆ Ioo a₂ b₂

Full source

@[gcongr]
theorem Ioo_subset_Ioo (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : IooIoo a₁ b₁ ⊆ Ioo a₂ b₂ := fun _ ⟨hx₁, hx₂⟩ =>
  ⟨h₁.trans_lt hx₁, hx₂.trans_le h₂⟩

Monotonicity of Open Interval Inclusion with Respect to Endpoints

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a preorder $\alpha$, if $a₂ \leq a₁$ and $b₁ \leq b₂$, then the open interval $(a₁, b₁)$ is a subset of the open interval $(a₂, b₂)$.

Set.Ioo_subset_Ioo_left theorem

(h : a₁ ≤ a₂) : Ioo a₂ b ⊆ Ioo a₁ b

Full source

@[gcongr]
theorem Ioo_subset_Ioo_left (h : a₁ ≤ a₂) : IooIoo a₂ b ⊆ Ioo a₁ b :=
  Ioo_subset_Ioo h le_rfl

Left Endpoint Monotonicity for Open Interval Inclusion

Informal description

For any elements $a₁, a₂, b$ in a preorder $\alpha$, if $a₁ \leq a₂$, then the open interval $(a₂, b)$ is a subset of the open interval $(a₁, b)$.

Set.Ioo_subset_Ioo_right theorem

(h : b₁ ≤ b₂) : Ioo a b₁ ⊆ Ioo a b₂

Full source

@[gcongr]
theorem Ioo_subset_Ioo_right (h : b₁ ≤ b₂) : IooIoo a b₁ ⊆ Ioo a b₂ :=
  Ioo_subset_Ioo le_rfl h

Right Endpoint Monotonicity for Open Interval Inclusion

Informal description

For any elements $a, b₁, b₂$ in a preorder $\alpha$, if $b₁ \leq b₂$, then the open interval $(a, b₁)$ is a subset of the open interval $(a, b₂)$.

Set.Ico_subset_Ico theorem

(h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : Ico a₁ b₁ ⊆ Ico a₂ b₂

Full source

@[gcongr]
theorem Ico_subset_Ico (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : IcoIco a₁ b₁ ⊆ Ico a₂ b₂ := fun _ ⟨hx₁, hx₂⟩ =>
  ⟨h₁.trans hx₁, hx₂.trans_le h₂⟩

Inclusion of Left-Closed Right-Open Intervals under Weakening Bounds

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a preorder $\alpha$, if $a₂ \leq a₁$ and $b₁ \leq b₂$, then the left-closed right-open interval $[a₁, b₁)$ is a subset of the left-closed right-open interval $[a₂, b₂)$.

Set.Ico_subset_Ico_left theorem

(h : a₁ ≤ a₂) : Ico a₂ b ⊆ Ico a₁ b

Full source

@[gcongr]
theorem Ico_subset_Ico_left (h : a₁ ≤ a₂) : IcoIco a₂ b ⊆ Ico a₁ b :=
  Ico_subset_Ico h le_rfl

Left-Weakening Inclusion of Left-Closed Right-Open Intervals

Informal description

For any elements $a₁, a₂, b$ in a preorder $\alpha$, if $a₁ \leq a₂$, then the left-closed right-open interval $[a₂, b)$ is a subset of the left-closed right-open interval $[a₁, b)$.

Set.Ico_subset_Ico_right theorem

(h : b₁ ≤ b₂) : Ico a b₁ ⊆ Ico a b₂

Full source

@[gcongr]
theorem Ico_subset_Ico_right (h : b₁ ≤ b₂) : IcoIco a b₁ ⊆ Ico a b₂ :=
  Ico_subset_Ico le_rfl h

Right-Weakening Inclusion of Left-Closed Right-Open Intervals

Informal description

For any elements $a, b₁, b₂$ in a preorder $\alpha$, if $b₁ \leq b₂$, then the left-closed right-open interval $[a, b₁)$ is a subset of the left-closed right-open interval $[a, b₂)$.

Set.Icc_subset_Icc theorem

(h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : Icc a₁ b₁ ⊆ Icc a₂ b₂

Full source

@[gcongr]
theorem Icc_subset_Icc (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : IccIcc a₁ b₁ ⊆ Icc a₂ b₂ := fun _ ⟨hx₁, hx₂⟩ =>
  ⟨h₁.trans hx₁, le_trans hx₂ h₂⟩

Inclusion of Closed Intervals under Monotonicity Conditions

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a preorder $\alpha$, if $a₂ \leq a₁$ and $b₁ \leq b₂$, then the closed interval $[a₁, b₁]$ is a subset of the closed interval $[a₂, b₂]$.

Set.Icc_subset_Icc_left theorem

(h : a₁ ≤ a₂) : Icc a₂ b ⊆ Icc a₁ b

Full source

@[gcongr]
theorem Icc_subset_Icc_left (h : a₁ ≤ a₂) : IccIcc a₂ b ⊆ Icc a₁ b :=
  Icc_subset_Icc h le_rfl

Left Monotonicity of Closed Interval Inclusion

Informal description

For any elements $a₁, a₂, b$ in a preorder $\alpha$, if $a₁ \leq a₂$, then the closed interval $[a₂, b]$ is a subset of the closed interval $[a₁, b]$.

Set.Icc_subset_Icc_right theorem

(h : b₁ ≤ b₂) : Icc a b₁ ⊆ Icc a b₂

Full source

@[gcongr]
theorem Icc_subset_Icc_right (h : b₁ ≤ b₂) : IccIcc a b₁ ⊆ Icc a b₂ :=
  Icc_subset_Icc le_rfl h

Right Monotonicity of Closed Interval Inclusion

Informal description

For any elements $a, b₁, b₂$ in a preorder $\alpha$, if $b₁ \leq b₂$, then the closed interval $[a, b₁]$ is a subset of the closed interval $[a, b₂]$.

Set.Icc_subset_Ioo theorem

(ha : a₂ < a₁) (hb : b₁ < b₂) : Icc a₁ b₁ ⊆ Ioo a₂ b₂

Full source

theorem Icc_subset_Ioo (ha : a₂ < a₁) (hb : b₁ < b₂) : IccIcc a₁ b₁ ⊆ Ioo a₂ b₂ := fun _ hx =>
  ⟨ha.trans_le hx.1, hx.2.trans_lt hb⟩

Inclusion of Closed Interval in Open Interval: $[a₁, b₁] \subseteq (a₂, b₂)$ under $a₂ < a₁$ and $b₁ < b₂$

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a preorder, if $a₂ < a₁$ and $b₁ < b₂$, then the closed interval $[a₁, b₁]$ is contained in the open interval $(a₂, b₂)$.

Set.Icc_subset_Ici_self theorem

: Icc a b ⊆ Ici a

Full source

theorem Icc_subset_Ici_self : IccIcc a b ⊆ Ici a := fun _ => And.left

Inclusion of Closed Interval in Left-Closed Right-Infinite Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the closed interval $[a, b]$ is a subset of the left-closed right-infinite interval $[a, \infty)$.

Set.Icc_subset_Iic_self theorem

: Icc a b ⊆ Iic b

Full source

theorem Icc_subset_Iic_self : IccIcc a b ⊆ Iic b := fun _ => And.right

Inclusion of Closed Interval in Left-Infinite Right-Closed Interval: $[a, b] \subseteq (-\infty, b]$

Informal description

For any elements $a$ and $b$ in a preorder, the closed interval $[a, b]$ is a subset of the left-infinite right-closed interval $(-\infty, b]$.

Set.Ioc_subset_Iic_self theorem

: Ioc a b ⊆ Iic b

Full source

theorem Ioc_subset_Iic_self : IocIoc a b ⊆ Iic b := fun _ => And.right

Inclusion of $(a, b]$ in $(-\infty, b]$

Informal description

For any elements $a$ and $b$ in a preorder, the left-open right-closed interval $(a, b]$ is a subset of the left-infinite right-closed interval $(-\infty, b]$.

Set.Ioc_subset_Ioc theorem

(h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : Ioc a₁ b₁ ⊆ Ioc a₂ b₂

Full source

@[gcongr]
theorem Ioc_subset_Ioc (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : IocIoc a₁ b₁ ⊆ Ioc a₂ b₂ := fun _ ⟨hx₁, hx₂⟩ =>
  ⟨h₁.trans_lt hx₁, hx₂.trans h₂⟩

Inclusion of Left-Open Right-Closed Intervals under Endpoint Conditions

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a preorder $\alpha$, if $a₂ \leq a₁$ and $b₁ \leq b₂$, then the left-open right-closed interval $(a₁, b₁]$ is contained in the interval $(a₂, b₂]$.

Set.Ioc_subset_Ioc_left theorem

(h : a₁ ≤ a₂) : Ioc a₂ b ⊆ Ioc a₁ b

Full source

@[gcongr]
theorem Ioc_subset_Ioc_left (h : a₁ ≤ a₂) : IocIoc a₂ b ⊆ Ioc a₁ b :=
  Ioc_subset_Ioc h le_rfl

Left Endpoint Monotonicity of Left-Open Right-Closed Intervals

Informal description

For any elements $a₁, a₂, b$ in a preorder $\alpha$, if $a₁ \leq a₂$, then the left-open right-closed interval $(a₂, b]$ is contained in the interval $(a₁, b]$.

Set.Ioc_subset_Ioc_right theorem

(h : b₁ ≤ b₂) : Ioc a b₁ ⊆ Ioc a b₂

Full source

@[gcongr]
theorem Ioc_subset_Ioc_right (h : b₁ ≤ b₂) : IocIoc a b₁ ⊆ Ioc a b₂ :=
  Ioc_subset_Ioc le_rfl h

Right Endpoint Monotonicity of Left-Open Right-Closed Intervals

Informal description

For any elements $a$, $b₁$, and $b₂$ in a preorder $\alpha$, if $b₁ \leq b₂$, then the left-open right-closed interval $(a, b₁]$ is contained in the interval $(a, b₂]$.

Set.Ico_subset_Ioo_left theorem

(h₁ : a₁ < a₂) : Ico a₂ b ⊆ Ioo a₁ b

Full source

theorem Ico_subset_Ioo_left (h₁ : a₁ < a₂) : IcoIco a₂ b ⊆ Ioo a₁ b := fun _ =>
  And.imp_left h₁.trans_le

Inclusion of Left-Closed Right-Open Interval in Open Interval Under Left Endpoint Shift

Informal description

For any elements $a_1, a_2, b$ in a preorder $\alpha$, if $a_1 < a_2$, then the left-closed right-open interval $[a_2, b)$ is contained in the open interval $(a_1, b)$.

Set.Ioc_subset_Ioo_right theorem

(h : b₁ < b₂) : Ioc a b₁ ⊆ Ioo a b₂

Full source

theorem Ioc_subset_Ioo_right (h : b₁ < b₂) : IocIoc a b₁ ⊆ Ioo a b₂ := fun _ =>
  And.imp_right fun h' => h'.trans_lt h

Inclusion of $(a, b₁]$ in $(a, b₂)$ when $b₁ < b₂$

Informal description

For any elements $a$, $b₁$, and $b₂$ in a preorder $\alpha$, if $b₁ < b₂$, then the left-open right-closed interval $(a, b₁]$ is a subset of the open interval $(a, b₂)$.

Set.Icc_subset_Ico_right theorem

(h₁ : b₁ < b₂) : Icc a b₁ ⊆ Ico a b₂

Full source

theorem Icc_subset_Ico_right (h₁ : b₁ < b₂) : IccIcc a b₁ ⊆ Ico a b₂ := fun _ =>
  And.imp_right fun h₂ => h₂.trans_lt h₁

Inclusion of Closed Interval in Left-Closed Right-Open Interval Under Right Endpoint Expansion

Informal description

For any elements $a, b_1, b_2$ in a preorder $\alpha$, if $b_1 < b_2$, then the closed interval $[a, b_1]$ is contained in the left-closed right-open interval $[a, b_2)$.

Set.Ioo_subset_Ico_self theorem

: Ioo a b ⊆ Ico a b

Full source

theorem Ioo_subset_Ico_self : IooIoo a b ⊆ Ico a b := fun _ => And.imp_left le_of_lt

Inclusion of Open Interval in Left-Closed Right-Open Interval

Informal description

For any elements $a$ and $b$ in a preorder, the open interval $(a, b)$ is a subset of the left-closed right-open interval $[a, b)$.

Set.Ioo_subset_Ioc_self theorem

: Ioo a b ⊆ Ioc a b

Full source

theorem Ioo_subset_Ioc_self : IooIoo a b ⊆ Ioc a b := fun _ => And.imp_right le_of_lt

Inclusion of Open Interval in Left-Open Right-Closed Interval

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, the open interval $(a, b)$ is a subset of the left-open right-closed interval $(a, b]$, i.e., $\text{Ioo}(a, b) \subseteq \text{Ioc}(a, b)$.

Set.Ico_subset_Icc_self theorem

: Ico a b ⊆ Icc a b

Full source

theorem Ico_subset_Icc_self : IcoIco a b ⊆ Icc a b := fun _ => And.imp_right le_of_lt

Inclusion of $\text{Ico}(a, b)$ in $\text{Icc}(a, b)$

Informal description

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

Set.Ioc_subset_Icc_self theorem

: Ioc a b ⊆ Icc a b

Full source

theorem Ioc_subset_Icc_self : IocIoc a b ⊆ Icc a b := fun _ => And.imp_left le_of_lt

Inclusion of $(a, b]$ in $[a, b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-open right-closed interval $(a, b]$ is a subset of the closed interval $[a, b]$.

Set.Ioo_subset_Icc_self theorem

: Ioo a b ⊆ Icc a b

Full source

theorem Ioo_subset_Icc_self : IooIoo a b ⊆ Icc a b :=
  Subset.trans Ioo_subset_Ico_self Ico_subset_Icc_self

Inclusion of Open Interval in Closed Interval: $(a, b) \subseteq [a, b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the open interval $(a, b)$ is a subset of the closed interval $[a, b]$, i.e., $\{x \mid a < x < b\} \subseteq \{x \mid a \leq x \leq b\}$.

Set.Ico_subset_Iio_self theorem

: Ico a b ⊆ Iio b

Full source

theorem Ico_subset_Iio_self : IcoIco a b ⊆ Iio b := fun _ => And.right

Inclusion of $[a, b)$ in $(-\infty, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-closed right-open interval $[a, b)$ is a subset of the left-infinite right-open interval $(-\infty, b)$.

Set.Ioo_subset_Iio_self theorem

: Ioo a b ⊆ Iio b

Full source

theorem Ioo_subset_Iio_self : IooIoo a b ⊆ Iio b := fun _ => And.right

Inclusion of Open Interval in Left-Infinite Right-Open Interval: $(a, b) \subseteq (-\infty, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the open interval $(a, b)$ is a subset of the left-infinite right-open interval $(-\infty, b)$, i.e., $(a, b) \subseteq (-\infty, b)$.

Set.Ioc_subset_Ioi_self theorem

: Ioc a b ⊆ Ioi a

Full source

theorem Ioc_subset_Ioi_self : IocIoc a b ⊆ Ioi a := fun _ => And.left

Inclusion of $(a, b]$ in $(a, \infty)$ in a preorder

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-open right-closed interval $(a, b]$ is a subset of the left-open right-infinite interval $(a, \infty)$.

Set.Ioo_subset_Ioi_self theorem

: Ioo a b ⊆ Ioi a

Full source

theorem Ioo_subset_Ioi_self : IooIoo a b ⊆ Ioi a := fun _ => And.left

Open Interval Subset of Left-Open Infinite Interval

Informal description

For any elements $a$ and $b$ in a preorder, the open interval $(a, b)$ is a subset of the left-open right-infinite interval $(a, \infty)$, i.e., $(a, b) \subseteq (a, \infty)$.

Set.Ioi_subset_Ici_self theorem

: Ioi a ⊆ Ici a

Full source

theorem Ioi_subset_Ici_self : IoiIoi a ⊆ Ici a := fun _ hx => le_of_lt hx

Inclusion of Open Interval in Closed Interval: $(a, \infty) \subseteq [a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-infinite interval $(a, \infty)$ is a subset of the left-closed right-infinite interval $[a, \infty)$.

Set.Iio_subset_Iic_self theorem

: Iio a ⊆ Iic a

Full source

theorem Iio_subset_Iic_self : IioIio a ⊆ Iic a := fun _ hx => le_of_lt hx

Inclusion of open interval in closed interval: $(-\infty, a) \subseteq (-\infty, a]$

Informal description

For any element $a$ in a preorder, the left-infinite right-open interval $(-\infty, a)$ is a subset of the left-infinite right-closed interval $(-\infty, a]$.

Set.Ico_subset_Ici_self theorem

: Ico a b ⊆ Ici a

Full source

theorem Ico_subset_Ici_self : IcoIco a b ⊆ Ici a := fun _ => And.left

Inclusion of Left-Closed Right-Open Interval in Left-Closed Right-Infinite Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-closed right-open interval $[a, b)$ is a subset of the left-closed right-infinite interval $[a, \infty)$. In other words, $[a, b) \subseteq [a, \infty)$.

Set.Ioi_ssubset_Ici_self theorem

: Ioi a ⊂ Ici a

Full source

theorem Ioi_ssubset_Ici_self : IoiIoi a ⊂ Ici a :=
  ⟨Ioi_subset_Ici_self, fun h => lt_irrefl a (h le_rfl)⟩

Proper Inclusion of Open Interval in Closed Interval: $(a, \infty) \subsetneq [a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-infinite interval $(a, \infty)$ is a proper subset of the left-closed right-infinite interval $[a, \infty)$.

Set.Iio_ssubset_Iic_self theorem

: Iio a ⊂ Iic a

Full source

theorem Iio_ssubset_Iic_self : IioIio a ⊂ Iic a :=
  @Ioi_ssubset_Ici_self αᵒᵈ _ _

Proper Inclusion of Open Interval in Closed Interval: $(-\infty, a) \subsetneq (-\infty, a]$

Informal description

For any element $a$ in a preorder $\alpha$, the left-infinite right-open interval $(-\infty, a)$ is a proper subset of the left-infinite right-closed interval $(-\infty, a]$.

Set.Icc_subset_Icc_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Full source

theorem Icc_subset_Icc_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Icc a₂ b₂Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
  ⟨fun h => ⟨(h ⟨le_rfl, h₁⟩).1, (h ⟨h₁, le_rfl⟩).2⟩, fun ⟨h, h'⟩ _ ⟨hx, hx'⟩ =>
    ⟨h.trans hx, hx'.trans h'⟩⟩

Subset Condition for Closed Intervals: $[a_1, b_1] \subseteq [a_2, b_2] \iff a_2 \leq a_1 \leq b_1 \leq b_2$

Informal description

For any elements $a_1, b_1, a_2, b_2$ in a preorder $\alpha$ such that $a_1 \leq b_1$, the closed interval $[a_1, b_1]$ is a subset of the closed interval $[a_2, b_2]$ if and only if $a_2 \leq a_1$ and $b_1 \leq b_2$.

Set.Icc_subset_Ioo_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

Full source

theorem Icc_subset_Ioo_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Ioo a₂ b₂Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂ :=
  ⟨fun h => ⟨(h ⟨le_rfl, h₁⟩).1, (h ⟨h₁, le_rfl⟩).2⟩, fun ⟨h, h'⟩ _ ⟨hx, hx'⟩ =>
    ⟨h.trans_le hx, hx'.trans_lt h'⟩⟩

Closed Interval Subset of Open Interval Criterion

Informal description

For any elements $a₁, b₁$ in a preorder with $a₁ \leq b₁$, the closed interval $[a₁, b₁]$ is a subset of the open interval $(a₂, b₂)$ if and only if $a₂ < a₁$ and $b₁ < b₂$.

Set.Icc_subset_Ico_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂

Full source

theorem Icc_subset_Ico_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Ico a₂ b₂Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂ :=
  ⟨fun h => ⟨(h ⟨le_rfl, h₁⟩).1, (h ⟨h₁, le_rfl⟩).2⟩, fun ⟨h, h'⟩ _ ⟨hx, hx'⟩ =>
    ⟨h.trans hx, hx'.trans_lt h'⟩⟩

Closed Interval Subset of Left-Closed Right-Open Interval Criterion

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a preorder $\alpha$ with $a₁ \leq b₁$, the closed interval $[a₁, b₁]$ is a subset of the left-closed right-open interval $[a₂, b₂)$ if and only if $a₂ \leq a₁$ and $b₁ < b₂$.

Set.Icc_subset_Ioc_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂

Full source

theorem Icc_subset_Ioc_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Ioc a₂ b₂Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂ :=
  ⟨fun h => ⟨(h ⟨le_rfl, h₁⟩).1, (h ⟨h₁, le_rfl⟩).2⟩, fun ⟨h, h'⟩ _ ⟨hx, hx'⟩ =>
    ⟨h.trans_le hx, hx'.trans h'⟩⟩

Subset Condition for Closed Interval in Left-Open Right-Closed Interval

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a preorder $\alpha$ with $a₁ \leq b₁$, the closed interval $[a₁, b₁]$ is a subset of the left-open right-closed interval $(a₂, b₂]$ if and only if $a₂ < a₁$ and $b₁ \leq b₂$.

Set.Icc_subset_Iio_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Iio b₂ ↔ b₁ < b₂

Full source

theorem Icc_subset_Iio_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Iio b₂Icc a₁ b₁ ⊆ Iio b₂ ↔ b₁ < b₂ :=
  ⟨fun h => h ⟨h₁, le_rfl⟩, fun h _ ⟨_, hx'⟩ => hx'.trans_lt h⟩

Closed Interval Subset of Left-Infinite Right-Open Interval Criterion

Informal description

For any elements $a₁$ and $b₁$ in a preorder $\alpha$ with $a₁ \leq b₁$, the closed interval $[a₁, b₁]$ is a subset of the left-infinite right-open interval $(-\infty, b₂)$ if and only if $b₁ < b₂$.

Set.Icc_subset_Ioi_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioi a₂ ↔ a₂ < a₁

Full source

theorem Icc_subset_Ioi_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Ioi a₂Icc a₁ b₁ ⊆ Ioi a₂ ↔ a₂ < a₁ :=
  ⟨fun h => h ⟨le_rfl, h₁⟩, fun h _ ⟨hx, _⟩ => h.trans_le hx⟩

Closed Interval Subset of Left-Open Right-Infinite Interval Criterion

Informal description

For any elements $a₁, b₁, a₂$ in a preorder $\alpha$ with $a₁ \leq b₁$, the closed interval $[a₁, b₁]$ is a subset of the left-open right-infinite interval $(a₂, \infty)$ if and only if $a₂ < a₁$.

Set.Icc_subset_Iic_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Iic b₂ ↔ b₁ ≤ b₂

Full source

theorem Icc_subset_Iic_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Iic b₂Icc a₁ b₁ ⊆ Iic b₂ ↔ b₁ ≤ b₂ :=
  ⟨fun h => h ⟨h₁, le_rfl⟩, fun h _ ⟨_, hx'⟩ => hx'.trans h⟩

Closed Interval Subset of Left-Infinite Right-Closed Interval Criterion

Informal description

For any elements $a₁$, $b₁$, and $b₂$ in a preorder $\alpha$ with $a₁ \leq b₁$, the closed interval $[a₁, b₁]$ is a subset of the left-infinite right-closed interval $(-\infty, b₂]$ if and only if $b₁ \leq b₂$.

Set.Icc_subset_Ici_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ici a₂ ↔ a₂ ≤ a₁

Full source

theorem Icc_subset_Ici_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Ici a₂Icc a₁ b₁ ⊆ Ici a₂ ↔ a₂ ≤ a₁ :=
  ⟨fun h => h ⟨le_rfl, h₁⟩, fun h _ ⟨hx, _⟩ => h.trans hx⟩

Inclusion of Closed Interval in Left-Closed Right-Infinite Interval

Informal description

For any elements $a₁, b₁, a₂$ in a preorder $\alpha$ with $a₁ \leq b₁$, the closed interval $[a₁, b₁]$ is a subset of the left-closed right-infinite interval $[a₂, \infty)$ if and only if $a₂ \leq a₁$.

Set.Icc_ssubset_Icc_left theorem

(hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) : Icc a₁ b₁ ⊂ Icc a₂ b₂

Full source

theorem Icc_ssubset_Icc_left (hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) : IccIcc a₁ b₁ ⊂ Icc a₂ b₂ :=
  (ssubset_iff_of_subset (Icc_subset_Icc (le_of_lt ha) hb)).mpr
    ⟨a₂, left_mem_Icc.mpr hI, not_and.mpr fun f _ => lt_irrefl a₂ (ha.trans_le f)⟩

Proper Subset Relation for Closed Intervals under Left Endpoint Strict Inequality

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a preorder such that $a₂ \leq b₂$, if $a₂ < a₁$ and $b₁ \leq b₂$, then the closed interval $[a₁, b₁]$ is a proper subset of the closed interval $[a₂, b₂]$.

Set.Icc_ssubset_Icc_right theorem

(hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) : Icc a₁ b₁ ⊂ Icc a₂ b₂

Full source

theorem Icc_ssubset_Icc_right (hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) :
    IccIcc a₁ b₁ ⊂ Icc a₂ b₂ :=
  (ssubset_iff_of_subset (Icc_subset_Icc ha (le_of_lt hb))).mpr
    ⟨b₂, right_mem_Icc.mpr hI, fun f => lt_irrefl b₁ (hb.trans_le f.2)⟩

Proper Subset Relation for Closed Intervals under Right Endpoint Strict Inequality

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a preorder such that $a₂ \leq b₂$, if $a₂ \leq a₁$ and $b₁ < b₂$, then the closed interval $[a₁, b₁]$ is a proper subset of the closed interval $[a₂, b₂]$.

Set.Ioi_subset_Ioi theorem

(h : a ≤ b) : Ioi b ⊆ Ioi a

Full source

/-- If `a ≤ b`, then `(b, +∞) ⊆ (a, +∞)`. In preorders, this is just an implication. If you need
the equivalence in linear orders, use `Ioi_subset_Ioi_iff`. -/
@[gcongr]
theorem Ioi_subset_Ioi (h : a ≤ b) : IoiIoi b ⊆ Ioi a := fun _ hx => h.trans_lt hx

Monotonicity of Right-Infinite Open Intervals: $(b, \infty) \subseteq (a, \infty)$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the right-infinite open interval $(b, \infty)$ is a subset of the right-infinite open interval $(a, \infty)$.

Set.Ioi_ssubset_Ioi theorem

(h : a < b) : Ioi b ⊂ Ioi a

Full source

/-- If `a < b`, then `(b, +∞) ⊂ (a, +∞)`. In preorders, this is just an implication. If you need
the equivalence in linear orders, use `Ioi_ssubset_Ioi_iff`. -/
@[gcongr]
theorem Ioi_ssubset_Ioi (h : a < b) : IoiIoi b ⊂ Ioi a :=
  (ssubset_iff_of_subset (Ioi_subset_Ioi h.le)).mpr ⟨b, h, lt_irrefl b⟩

Proper Subset Relation for Right-Infinite Open Intervals: $(b, \infty) \subset (a, \infty)$ when $a < b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a < b$, the right-infinite open interval $(b, \infty)$ is a proper subset of $(a, \infty)$.

Set.Ioi_subset_Ici theorem

(h : a ≤ b) : Ioi b ⊆ Ici a

Full source

/-- If `a ≤ b`, then `(b, +∞) ⊆ [a, +∞)`. In preorders, this is just an implication. If you need
the equivalence in dense linear orders, use `Ioi_subset_Ici_iff`. -/
theorem Ioi_subset_Ici (h : a ≤ b) : IoiIoi b ⊆ Ici a :=
  Subset.trans (Ioi_subset_Ioi h) Ioi_subset_Ici_self

Inclusion of Open Interval in Closed Interval: $(b, \infty) \subseteq [a, \infty)$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the right-infinite open interval $(b, \infty)$ is a subset of the right-infinite closed interval $[a, \infty)$.

Set.Iio_subset_Iio theorem

(h : a ≤ b) : Iio a ⊆ Iio b

Full source

/-- If `a ≤ b`, then `(-∞, a) ⊆ (-∞, b)`. In preorders, this is just an implication. If you need
the equivalence in linear orders, use `Iio_subset_Iio_iff`. -/
@[gcongr]
theorem Iio_subset_Iio (h : a ≤ b) : IioIio a ⊆ Iio b := fun _ hx => lt_of_lt_of_le hx h

Monotonicity of Left-Infinite Right-Open Intervals with Respect to Order

Informal description

For any elements $a$ and $b$ in a preorder, if $a \leq b$, then the left-infinite right-open interval $(-\infty, a)$ is a subset of the interval $(-\infty, b)$, i.e., $\{x \mid x < a\} \subseteq \{x \mid x < b\}$.

Set.Iio_ssubset_Iio theorem

(h : a < b) : Iio a ⊂ Iio b

Full source

/-- If `a < b`, then `(-∞, a) ⊂ (-∞, b)`. In preorders, this is just an implication. If you need
the equivalence in linear orders, use `Iio_ssubset_Iio_iff`. -/
@[gcongr]
theorem Iio_ssubset_Iio (h : a < b) : IioIio a ⊂ Iio b :=
  (ssubset_iff_of_subset (Iio_subset_Iio h.le)).mpr ⟨a, h, lt_irrefl a⟩

Strict Monotonicity of Left-Infinite Right-Open Intervals: $a < b \Rightarrow (-\infty, a) \subsetneq (-\infty, b)$

Informal description

For any elements $a$ and $b$ in a preorder, if $a < b$, then the left-infinite right-open interval $(-\infty, a)$ is a proper subset of the interval $(-\infty, b)$, i.e., $\{x \mid x < a\} \subsetneq \{x \mid x < b\}$.

Set.Iio_subset_Iic theorem

(h : a ≤ b) : Iio a ⊆ Iic b

Full source

/-- If `a ≤ b`, then `(-∞, a) ⊆ (-∞, b]`. In preorders, this is just an implication. If you need
the equivalence in dense linear orders, use `Iio_subset_Iic_iff`. -/
theorem Iio_subset_Iic (h : a ≤ b) : IioIio a ⊆ Iic b :=
  Subset.trans (Iio_subset_Iio h) Iio_subset_Iic_self

Inclusion of Open Interval in Closed Interval: $a \leq b \Rightarrow (-\infty, a) \subseteq (-\infty, b]$

Informal description

For any elements $a$ and $b$ in a preorder, if $a \leq b$, then the left-infinite right-open interval $(-\infty, a)$ is a subset of the left-infinite right-closed interval $(-\infty, b]$, i.e., $\{x \mid x < a\} \subseteq \{x \mid x \leq b\}$.

Set.Ici_inter_Iic theorem

: Ici a ∩ Iic b = Icc a b

Full source

theorem Ici_inter_Iic : IciIci a ∩ Iic b = Icc a b :=
  rfl

Intersection of $[a, \infty)$ and $(-\infty, b]$ is $[a, b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the intersection of the left-closed right-infinite interval $[a, \infty)$ and the left-infinite right-closed interval $(-\infty, b]$ equals the closed interval $[a, b]$, i.e., $$ [a, \infty) \cap (-\infty, b] = [a, b]. $$

Set.Ici_inter_Iio theorem

: Ici a ∩ Iio b = Ico a b

Full source

theorem Ici_inter_Iio : IciIci a ∩ Iio b = Ico a b :=
  rfl

Intersection of $[a, \infty)$ and $(-\infty, b)$ is $[a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the intersection of the left-closed right-infinite interval $[a, \infty)$ and the left-infinite right-open interval $(-\infty, b)$ equals the left-closed right-open interval $[a, b)$. In symbols: $$ [a, \infty) \cap (-\infty, b) = [a, b) $$

Set.Ioi_inter_Iic theorem

: Ioi a ∩ Iic b = Ioc a b

Full source

theorem Ioi_inter_Iic : IoiIoi a ∩ Iic b = Ioc a b :=
  rfl

Intersection of $(a, \infty)$ and $(-\infty, b]$ is $(a, b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the intersection of the left-open right-infinite interval $(a, \infty)$ and the left-infinite right-closed interval $(-\infty, b]$ is equal to the left-open right-closed interval $(a, b]$. In symbols: $$ (a, \infty) \cap (-\infty, b] = (a, b] $$

Set.Ioi_inter_Iio theorem

: Ioi a ∩ Iio b = Ioo a b

Full source

theorem Ioi_inter_Iio : IoiIoi a ∩ Iio b = Ioo a b :=
  rfl

Intersection of Left-Open and Right-Open Intervals Equals Open Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the intersection of the left-open right-infinite interval $(a, \infty)$ and the left-infinite right-open interval $(-\infty, b)$ is equal to the open interval $(a, b)$. That is, $(a, \infty) \cap (-\infty, b) = (a, b)$.

Set.Iic_inter_Ici theorem

: Iic a ∩ Ici b = Icc b a

Full source

theorem Iic_inter_Ici : IicIic a ∩ Ici b = Icc b a :=
  inter_comm _ _

Intersection of $(-\infty, a]$ and $[b, \infty)$ is $[b, a]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the intersection of the left-infinite right-closed interval $(-\infty, a]$ and the left-closed right-infinite interval $[b, \infty)$ is equal to the closed interval $[b, a]$, i.e., $(-\infty, a] \cap [b, \infty) = [b, a]$.

Set.Iio_inter_Ici theorem

: Iio a ∩ Ici b = Ico b a

Full source

theorem Iio_inter_Ici : IioIio a ∩ Ici b = Ico b a :=
  inter_comm _ _

Intersection of $(-\infty, a)$ and $[b, \infty)$ is $[b, a)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the intersection of the left-infinite right-open interval $(-\infty, a)$ and the left-closed right-infinite interval $[b, \infty)$ is equal to the left-closed right-open interval $[b, a)$, i.e., $$ (-\infty, a) \cap [b, \infty) = [b, a). $$

Set.Iic_inter_Ioi theorem

: Iic a ∩ Ioi b = Ioc b a

Full source

theorem Iic_inter_Ioi : IicIic a ∩ Ioi b = Ioc b a :=
  inter_comm _ _

Intersection of $(-\infty, a]$ and $(b, \infty)$ is $(b, a]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the intersection of the left-infinite right-closed interval $(-\infty, a]$ and the left-open right-infinite interval $(b, \infty)$ is equal to the left-open right-closed interval $(b, a]$, i.e., $(-\infty, a] \cap (b, \infty) = (b, a]$.

Set.Iio_inter_Ioi theorem

: Iio a ∩ Ioi b = Ioo b a

Full source

theorem Iio_inter_Ioi : IioIio a ∩ Ioi b = Ioo b a :=
  inter_comm _ _

Intersection of Left-Infinite and Right-Infinite Intervals Equals Open Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the intersection of the left-infinite right-open interval $(-\infty, a)$ and the left-open right-infinite interval $(b, \infty)$ is equal to the open interval $(b, a)$. In symbols: \[ (-\infty, a) \cap (b, \infty) = (b, a). \]

Set.mem_Icc_of_Ioo theorem

(h : x ∈ Ioo a b) : x ∈ Icc a b

Full source

theorem mem_Icc_of_Ioo (h : x ∈ Ioo a b) : x ∈ Icc a b :=
  Ioo_subset_Icc_self h

Inclusion of Open Interval in Closed Interval

Informal description

For any elements $a$, $b$, and $x$ in a preorder, if $x$ belongs to the open interval $(a, b)$, then $x$ also belongs to the closed interval $[a, b]$. In symbols: \[ x \in (a, b) \implies x \in [a, b]. \]

Set.mem_Ico_of_Ioo theorem

(h : x ∈ Ioo a b) : x ∈ Ico a b

Full source

theorem mem_Ico_of_Ioo (h : x ∈ Ioo a b) : x ∈ Ico a b :=
  Ioo_subset_Ico_self h

Inclusion of Open Interval in Left-Closed Right-Open Interval

Informal description

For any elements $a$, $b$, and $x$ in a preorder, if $x$ belongs to the open interval $(a, b)$, then $x$ also belongs to the left-closed right-open interval $[a, b)$. In symbols: \[ x \in (a, b) \implies x \in [a, b). \]

Set.mem_Ioc_of_Ioo theorem

(h : x ∈ Ioo a b) : x ∈ Ioc a b

Full source

theorem mem_Ioc_of_Ioo (h : x ∈ Ioo a b) : x ∈ Ioc a b :=
  Ioo_subset_Ioc_self h

Inclusion of Open Interval in Left-Open Right-Closed Interval

Informal description

For any elements $a$, $b$, and $x$ in a preorder, if $x$ belongs to the open interval $(a, b)$, then $x$ also belongs to the left-open right-closed interval $(a, b]$. In symbols: \[ x \in (a, b) \implies x \in (a, b]. \]

Set.mem_Icc_of_Ico theorem

(h : x ∈ Ico a b) : x ∈ Icc a b

Full source

theorem mem_Icc_of_Ico (h : x ∈ Ico a b) : x ∈ Icc a b :=
  Ico_subset_Icc_self h

Inclusion of $[a, b)$ in $[a, b]$

Informal description

For any elements $a$, $b$, and $x$ in a preorder, if $x$ belongs to the left-closed right-open interval $[a, b)$, then $x$ also belongs to the closed interval $[a, b]$. In symbols: \[ x \in [a, b) \implies x \in [a, b]. \]

Set.mem_Icc_of_Ioc theorem

(h : x ∈ Ioc a b) : x ∈ Icc a b

Full source

theorem mem_Icc_of_Ioc (h : x ∈ Ioc a b) : x ∈ Icc a b :=
  Ioc_subset_Icc_self h

Inclusion of $(a, b]$ in $[a, b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, if $x$ belongs to the left-open right-closed interval $(a, b]$, then $x$ also belongs to the closed interval $[a, b]$.

Set.mem_Ici_of_Ioi theorem

(h : x ∈ Ioi a) : x ∈ Ici a

Full source

theorem mem_Ici_of_Ioi (h : x ∈ Ioi a) : x ∈ Ici a :=
  Ioi_subset_Ici_self h

Inclusion from $(a, \infty)$ to $[a, \infty)$

Informal description

For any element $x$ in a preorder, if $x$ belongs to the left-open right-infinite interval $(a, \infty)$, then $x$ also belongs to the left-closed right-infinite interval $[a, \infty)$.

Set.mem_Iic_of_Iio theorem

(h : x ∈ Iio a) : x ∈ Iic a

Full source

theorem mem_Iic_of_Iio (h : x ∈ Iio a) : x ∈ Iic a :=
  Iio_subset_Iic_self h

Inclusion from open to closed left-infinite interval: $(-\infty, a) \subseteq (-\infty, a]$

Informal description

For any element $x$ in a preorder, if $x$ belongs to the left-infinite right-open interval $(-\infty, a)$, then $x$ also belongs to the left-infinite right-closed interval $(-\infty, a]$.

Set.Icc_eq_empty_iff theorem

: Icc a b = ∅ ↔ ¬a ≤ b

Full source

theorem Icc_eq_empty_iff : IccIcc a b = ∅ ↔ ¬a ≤ b := by
  rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Icc]

Empty Closed Interval Criterion: $[a, b] = \emptyset \leftrightarrow a \nleq b$

Informal description

For any elements $a$ and $b$ in a preorder, the closed interval $[a, b]$ is empty if and only if $a \nleq b$.

Set.Ico_eq_empty_iff theorem

: Ico a b = ∅ ↔ ¬a < b

Full source

theorem Ico_eq_empty_iff : IcoIco a b = ∅ ↔ ¬a < b := by
  rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ico]

Empty Left-Closed Right-Open Interval Criterion: $[a, b) = \emptyset \leftrightarrow a \geq b$

Informal description

For any elements $a$ and $b$ in a preorder, the left-closed right-open interval $[a, b)$ is empty if and only if $a \nless b$.

Set.Ioc_eq_empty_iff theorem

: Ioc a b = ∅ ↔ ¬a < b

Full source

theorem Ioc_eq_empty_iff : IocIoc a b = ∅ ↔ ¬a < b := by
  rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioc]

Empty Left-Open Right-Closed Interval Criterion: $(a, b] = \emptyset \leftrightarrow a \geq b$

Informal description

For any elements $a$ and $b$ in a preorder, the left-open right-closed interval $(a, b]$ is empty if and only if $a \geq b$.

Set.Ioo_eq_empty_iff theorem

[DenselyOrdered α] : Ioo a b = ∅ ↔ ¬a < b

Full source

theorem Ioo_eq_empty_iff [DenselyOrdered α] : IooIoo a b = ∅ ↔ ¬a < b := by
  rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioo]

Empty Open Interval Criterion in Densely Ordered Sets

Informal description

In a densely ordered set $\alpha$, the open interval $(a, b)$ is empty if and only if $a \geq b$.

IsTop.Iic_eq theorem

(h : IsTop a) : Iic a = univ

Full source

theorem _root_.IsTop.Iic_eq (h : IsTop a) : Iic a = univ :=
  eq_univ_of_forall h

Top Element Characterizes Universal Interval $(-\infty, a] = \alpha$

Informal description

For an element $a$ in a preorder $\alpha$, if $a$ is a top element (i.e., $a \geq b$ for all $b \in \alpha$), then the left-infinite right-closed interval $(-\infty, a]$ is equal to the entire set $\alpha$.

IsBot.Ici_eq theorem

(h : IsBot a) : Ici a = univ

Full source

theorem _root_.IsBot.Ici_eq (h : IsBot a) : Ici a = univ :=
  eq_univ_of_forall h

Bottom Element Makes Closed-Infinite Interval Universal

Informal description

If $a$ is a bottom element in a preorder $\alpha$, then the left-closed right-infinite interval $[a, \infty)$ is equal to the entire set $\alpha$.

Set.Ioi_eq_empty_iff theorem

: Ioi a = ∅ ↔ IsMax a

Full source

@[simp] theorem Ioi_eq_empty_iff : IoiIoi a = ∅ ↔ IsMax a := by
  simp only [isMax_iff_forall_not_lt, eq_empty_iff_forall_not_mem, mem_Ioi]

Empty Right-Infinite Interval Characterizes Maximal Elements

Informal description

For an element $a$ in a preorder, the set of elements strictly greater than $a$ is empty if and only if $a$ is a maximal element.

Set.Iio_eq_empty_iff theorem

: Iio a = ∅ ↔ IsMin a

Full source

@[simp] theorem Iio_eq_empty_iff : IioIio a = ∅ ↔ IsMin a := Ioi_eq_empty_iff (α := αᵒᵈ)

Empty Left-Infinite Interval Characterizes Minimal Elements

Informal description

For an element $a$ in a preorder, the left-infinite right-open interval $(-\infty, a)$ is empty if and only if $a$ is a minimal element.

Set.Iio_nonempty theorem

: (Iio a).Nonempty ↔ ¬IsMin a

Full source

@[simp] lemma Iio_nonempty : (Iio a).Nonempty ↔ ¬ IsMin a := by simp [nonempty_iff_ne_empty]

Nonemptiness of $(-\infty, a)$ Equivalent to Non-Minimality of $a$

Informal description

The left-infinite right-open interval $(-\infty, a)$ is nonempty if and only if $a$ is not a minimal element in the preorder.

Set.Ioi_nonempty theorem

: (Ioi a).Nonempty ↔ ¬IsMax a

Full source

@[simp] lemma Ioi_nonempty : (Ioi a).Nonempty ↔ ¬ IsMax a := by simp [nonempty_iff_ne_empty]

Nonemptiness of $(a, \infty)$ ↔ $a$ is not maximal

Informal description

The left-open right-infinite interval $(a, \infty)$ is nonempty if and only if $a$ is not a maximal element in the preorder.

Set.Iic_inter_Ioc_of_le theorem

(h : a ≤ c) : Iic a ∩ Ioc b c = Ioc b a

Full source

theorem Iic_inter_Ioc_of_le (h : a ≤ c) : IicIic a ∩ Ioc b c = Ioc b a :=
  ext fun _ => ⟨fun H => ⟨H.2.1, H.1⟩, fun H => ⟨H.2, H.1, H.2.trans h⟩⟩

Intersection of $(-\infty, a]$ and $(b, c]$ is $(b, a]$ when $a \leq c$

Informal description

For any elements $a$, $b$, and $c$ in a preorder $\alpha$ such that $a \leq c$, the intersection of the left-infinite right-closed interval $(-\infty, a]$ and the left-open right-closed interval $(b, c]$ is equal to the left-open right-closed interval $(b, a]$. That is, $$ (-\infty, a] \cap (b, c] = (b, a]. $$

Set.not_mem_Icc_of_lt theorem

(ha : c < a) : c ∉ Icc a b

Full source

theorem not_mem_Icc_of_lt (ha : c < a) : c ∉ Icc a b := fun h => ha.not_le h.1

Non-membership in Closed Interval Due to Left Strict Inequality

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $c < a$, then $c$ does not belong to the closed interval $[a, b]$.

Set.not_mem_Icc_of_gt theorem

(hb : b < c) : c ∉ Icc a b

Full source

theorem not_mem_Icc_of_gt (hb : b < c) : c ∉ Icc a b := fun h => hb.not_le h.2

Non-membership in Closed Interval Due to Right Strict Inequality

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b < c$, then $c$ does not belong to the closed interval $[a, b]$.

Set.not_mem_Ico_of_lt theorem

(ha : c < a) : c ∉ Ico a b

Full source

theorem not_mem_Ico_of_lt (ha : c < a) : c ∉ Ico a b := fun h => ha.not_le h.1

Non-membership in Left-Closed Right-Open Interval Due to Left Strict Inequality

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $c < a$, then $c$ does not belong to the left-closed right-open interval $[a, b)$.

Set.not_mem_Ioc_of_gt theorem

(hb : b < c) : c ∉ Ioc a b

Full source

theorem not_mem_Ioc_of_gt (hb : b < c) : c ∉ Ioc a b := fun h => hb.not_le h.2

Exclusion from Left-Open Right-Closed Interval by Greater Element

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b < c$, then $c$ does not belong to the left-open right-closed interval $(a, b]$.

Set.not_mem_Ioi_self theorem

: a ∉ Ioi a

Full source

theorem not_mem_Ioi_self : a ∉ Ioi a := lt_irrefl _

Self-exclusion from right-infinite open interval

Informal description

For any element $a$ in a preorder, $a$ does not belong to the interval $(a, \infty)$, i.e., $a \notin (a, \infty)$.

Set.not_mem_Iio_self theorem

: b ∉ Iio b

Full source

theorem not_mem_Iio_self : b ∉ Iio b := lt_irrefl _

Element Not in Its Own Left-Infinite Open Interval

Informal description

For any element $b$ in a preorder, $b$ does not belong to the interval $(-\infty, b)$, i.e., $b \notin (-\infty, b)$.

Set.not_mem_Ioc_of_le theorem

(ha : c ≤ a) : c ∉ Ioc a b

Full source

theorem not_mem_Ioc_of_le (ha : c ≤ a) : c ∉ Ioc a b := fun h => lt_irrefl _ <| h.1.trans_le ha

Non-membership in Left-Open Right-Closed Interval Under Left Bound Condition

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $c \leq a$, then $c$ does not belong to the left-open right-closed interval $(a, b]$.

Set.not_mem_Ico_of_ge theorem

(hb : b ≤ c) : c ∉ Ico a b

Full source

theorem not_mem_Ico_of_ge (hb : b ≤ c) : c ∉ Ico a b := fun h => lt_irrefl _ <| h.2.trans_le hb

Non-membership in Left-Closed Right-Open Interval under Greater-Than Condition

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b \leq c$, then $c$ does not belong to the left-closed right-open interval $[a, b)$.

Set.not_mem_Ioo_of_le theorem

(ha : c ≤ a) : c ∉ Ioo a b

Full source

theorem not_mem_Ioo_of_le (ha : c ≤ a) : c ∉ Ioo a b := fun h => lt_irrefl _ <| h.1.trans_le ha

Non-membership in open interval from left bound: $c \leq a \implies c \notin (a, b)$

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $c \leq a$, then $c$ does not belong to the open interval $(a, b)$.

Set.not_mem_Ioo_of_ge theorem

(hb : b ≤ c) : c ∉ Ioo a b

Full source

theorem not_mem_Ioo_of_ge (hb : b ≤ c) : c ∉ Ioo a b := fun h => lt_irrefl _ <| h.2.trans_le hb

Non-membership in Open Interval from Above: $b \leq c \implies c \notin (a, b)$

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $b \leq c$, then $c$ does not belong to the open interval $(a, b)$.

Set.Icc_eq_Ioc_same_iff theorem

: Icc a b = Ioc a b ↔ ¬a ≤ b

Full source

@[simp] theorem Icc_eq_Ioc_same_iff : IccIcc a b = Ioc a b ↔ ¬a ≤ b where
  mp h := by simpa using Set.ext_iff.mp h a
  mpr h := by rw [Icc_eq_empty h, Ioc_eq_empty (mt le_of_lt h)]

Equivalence of Closed and Left-Open Right-Closed Intervals When Not $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder, the closed interval $[a, b]$ is equal to the left-open right-closed interval $(a, b]$ if and only if $a \not\leq b$.

Set.Icc_eq_Ico_same_iff theorem

: Icc a b = Ico a b ↔ ¬a ≤ b

Full source

@[simp] theorem Icc_eq_Ico_same_iff : IccIcc a b = Ico a b ↔ ¬a ≤ b where
  mp h := by simpa using Set.ext_iff.mp h b
  mpr h := by rw [Icc_eq_empty h, Ico_eq_empty (mt le_of_lt h)]

Equality of Closed and Left-Closed Right-Open Intervals: $[a, b] = [a, b) ↔ a \not\leq b$

Informal description

For any elements $a$ and $b$ in a preorder, the closed interval $[a, b]$ is equal to the left-closed right-open interval $[a, b)$ if and only if $a \not\leq b$.

Set.Icc_eq_Ioo_same_iff theorem

: Icc a b = Ioo a b ↔ ¬a ≤ b

Full source

@[simp] theorem Icc_eq_Ioo_same_iff : IccIcc a b = Ioo a b ↔ ¬a ≤ b where
  mp h := by simpa using Set.ext_iff.mp h b
  mpr h := by rw [Icc_eq_empty h, Ioo_eq_empty (mt le_of_lt h)]

Equality of Closed and Open Intervals: $[a, b] = (a, b) ↔ a \not\leq b$

Informal description

For any elements $a$ and $b$ in a preorder, the closed interval $[a, b]$ equals the open interval $(a, b)$ if and only if $a \not\leq b$.

Set.Ioc_eq_Ico_same_iff theorem

: Ioc a b = Ico a b ↔ ¬a < b

Full source

@[simp] theorem Ioc_eq_Ico_same_iff : IocIoc a b = Ico a b ↔ ¬a < b where
  mp h := by simpa using Set.ext_iff.mp h a
  mpr h := by rw [Ioc_eq_empty h, Ico_eq_empty h]

Equality of Left-Open Right-Closed and Left-Closed Right-Open Intervals: $(a, b] = [a, b) ↔ ¬(a < b)$

Informal description

For any two elements $a$ and $b$ in a preorder, the left-open right-closed interval $(a, b]$ equals the left-closed right-open interval $[a, b)$ if and only if $a$ is not strictly less than $b$.

Set.Ioo_eq_Ioc_same_iff theorem

: Ioo a b = Ioc a b ↔ ¬a < b

Full source

@[simp] theorem Ioo_eq_Ioc_same_iff : IooIoo a b = Ioc a b ↔ ¬a < b where
  mp h := by simpa using Set.ext_iff.mp h b
  mpr h := by rw [Ioo_eq_empty h, Ioc_eq_empty h]

Equality of Open and Left-Open Right-Closed Intervals: $(a, b) = (a, b] ↔ ¬(a < b)$

Informal description

For any two elements $a$ and $b$ in a preorder, the open interval $(a, b)$ equals the left-open right-closed interval $(a, b]$ if and only if $a$ is not strictly less than $b$.

Set.Ioo_eq_Ico_same_iff theorem

: Ioo a b = Ico a b ↔ ¬a < b

Full source

@[simp] theorem Ioo_eq_Ico_same_iff : IooIoo a b = Ico a b ↔ ¬a < b where
  mp h := by simpa using Set.ext_iff.mp h a
  mpr h := by rw [Ioo_eq_empty h, Ico_eq_empty h]

Equality of Open and Left-Closed Right-Open Intervals: $(a, b) = [a, b) ↔ ¬(a < b)$

Informal description

For any two elements $a$ and $b$ in a preorder, the open interval $(a, b)$ equals the left-closed right-open interval $[a, b)$ if and only if $a$ is not strictly less than $b$.

Set.Ioc_eq_Icc_same_iff theorem

: Ioc a b = Icc a b ↔ ¬a ≤ b

Full source

@[simp] theorem Ioc_eq_Icc_same_iff : IocIoc a b = Icc a b ↔ ¬a ≤ b :=
  eq_comm.trans Icc_eq_Ioc_same_iff

Equality of $(a, b]$ and $[a, b]$ Intervals When Not $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder, the left-open right-closed interval $(a, b]$ is equal to the closed interval $[a, b]$ if and only if $a \not\leq b$.

Set.Ico_eq_Icc_same_iff theorem

: Ico a b = Icc a b ↔ ¬a ≤ b

Full source

@[simp] theorem Ico_eq_Icc_same_iff : IcoIco a b = Icc a b ↔ ¬a ≤ b :=
  eq_comm.trans Icc_eq_Ico_same_iff

Equality of Left-Closed Right-Open and Closed Intervals: $[a, b) = [a, b] ↔ a \not\leq b$

Informal description

For any elements $a$ and $b$ in a preorder, the left-closed right-open interval $[a, b)$ equals the closed interval $[a, b]$ if and only if $a \not\leq b$.

Set.Ioo_eq_Icc_same_iff theorem

: Ioo a b = Icc a b ↔ ¬a ≤ b

Full source

@[simp] theorem Ioo_eq_Icc_same_iff : IooIoo a b = Icc a b ↔ ¬a ≤ b :=
  eq_comm.trans Icc_eq_Ioo_same_iff

Equality of Open and Closed Intervals: $(a, b) = [a, b] ↔ a \not\leq b$

Informal description

For any elements $a$ and $b$ in a preorder, the open interval $(a, b)$ equals the closed interval $[a, b]$ if and only if $a \not\leq b$.

Set.Ico_eq_Ioc_same_iff theorem

: Ico a b = Ioc a b ↔ ¬a < b

Full source

@[simp] theorem Ico_eq_Ioc_same_iff : IcoIco a b = Ioc a b ↔ ¬a < b :=
  eq_comm.trans Ioc_eq_Ico_same_iff

Equality of Left-Closed Right-Open and Left-Open Right-Closed Intervals: $[a, b) = (a, b] ↔ ¬(a < b)$

Informal description

For any two elements $a$ and $b$ in a preorder, the left-closed right-open interval $[a, b)$ equals the left-open right-closed interval $(a, b]$ if and only if $a$ is not strictly less than $b$.

Set.Ioc_eq_Ioo_same_iff theorem

: Ioc a b = Ioo a b ↔ ¬a < b

Full source

@[simp] theorem Ioc_eq_Ioo_same_iff : IocIoc a b = Ioo a b ↔ ¬a < b :=
  eq_comm.trans Ioo_eq_Ioc_same_iff

Equality of Left-Open Right-Closed and Open Intervals: $(a, b] = (a, b) ↔ ¬(a < b)$

Informal description

For any two elements $a$ and $b$ in a preorder, the left-open right-closed interval $(a, b]$ equals the open interval $(a, b)$ if and only if $a$ is not strictly less than $b$.

Set.Ico_eq_Ioo_same_iff theorem

: Ico a b = Ioo a b ↔ ¬a < b

Full source

@[simp] theorem Ico_eq_Ioo_same_iff : IcoIco a b = Ioo a b ↔ ¬a < b :=
  eq_comm.trans Ioo_eq_Ico_same_iff

Equality of Left-Closed Right-Open and Open Intervals: $[a, b) = (a, b) ↔ ¬(a < b)$

Informal description

For any two elements $a$ and $b$ in a preorder, the left-closed right-open interval $[a, b)$ equals the open interval $(a, b)$ if and only if $a$ is not strictly less than $b$.

Set.Icc_self theorem

(a : α) : Icc a a = { a }

Full source

@[simp]
theorem Icc_self (a : α) : Icc a a = {a} :=
  Set.ext <| by simp [Icc, le_antisymm_iff, and_comm]

Closed Interval at a Point is Singleton: $[a, a] = \{a\}$

Informal description

For any element $ a $ in a preorder $ \alpha $, the closed interval $[a, a]$ is equal to the singleton set $\{a\}$.

Set.instIccUnique instance

: Unique (Set.Icc a a)

Full source

instance instIccUnique : Unique (Set.Icc a a) where
  default := ⟨a, by simp⟩
  uniq y := Subtype.ext <| by simpa using y.2

Uniqueness of Singleton Interval $[a, a]$

Informal description

For any element $a$ in a preorder $\alpha$, the closed interval $[a, a]$ has a unique element, namely $a$ itself.

Set.Icc_eq_singleton_iff theorem

: Icc a b = { c } ↔ a = c ∧ b = c

Full source

@[simp]
theorem Icc_eq_singleton_iff : IccIcc a b = {c} ↔ a = c ∧ b = c := by
  refine ⟨fun h => ?_, ?_⟩
  · have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst <| singleton_nonempty c)
    exact
      ⟨eq_of_mem_singleton <| h ▸ left_mem_Icc.2 hab,
        eq_of_mem_singleton <| h ▸ right_mem_Icc.2 hab⟩
  · rintro ⟨rfl, rfl⟩
    exact Icc_self _

Singleton Interval Characterization: $[a, b] = \{c\} \leftrightarrow a = c = b$

Informal description

For any elements $a$, $b$, and $c$ in a preorder, the closed interval $[a, b]$ is equal to the singleton set $\{c\}$ if and only if $a = c$ and $b = c$.

Set.subsingleton_Icc_of_ge theorem

(hba : b ≤ a) : Set.Subsingleton (Icc a b)

Full source

lemma subsingleton_Icc_of_ge (hba : b ≤ a) : Set.Subsingleton (Icc a b) :=
  fun _x ⟨hax, hxb⟩ _y ⟨hay, hyb⟩ ↦ le_antisymm
    (le_implies_le_of_le_of_le hxb hay hba) (le_implies_le_of_le_of_le hyb hax hba)

Closed interval $[a, b]$ is subsingleton when $b \leq a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, if $b \leq a$, then the closed interval $[a, b]$ is a subsingleton (i.e., contains at most one element).

Set.subsingleton_Icc_iff theorem

{α : Type*} [LinearOrder α] {a b : α} : Set.Subsingleton (Icc a b) ↔ b ≤ a

Full source

@[simp] lemma subsingleton_Icc_iff {α : Type*} [LinearOrder α] {a b : α} :
    Set.SubsingletonSet.Subsingleton (Icc a b) ↔ b ≤ a := by
  refine ⟨fun h ↦ ?_, subsingleton_Icc_of_ge⟩
  contrapose! h
  simp only [gt_iff_lt, not_subsingleton_iff]
  exact ⟨a, ⟨le_refl _, h.le⟩, b, ⟨h.le, le_refl _⟩, h.ne⟩

Subsingleton Characterization of Closed Intervals in Linear Orders

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the closed interval $[a, b]$ is a subsingleton (i.e., contains at most one element) if and only if $b \leq a$.

Set.Icc_diff_left theorem

: Icc a b \ { a } = Ioc a b

Full source

@[simp]
theorem Icc_diff_left : IccIcc a b \ {a} = Ioc a b :=
  ext fun x => by simp [lt_iff_le_and_ne, eq_comm, and_right_comm]

Difference of Closed Interval and Left Endpoint Equals Left-Open Right-Closed Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the set difference between the closed interval $[a, b]$ and the singleton set $\{a\}$ is equal to the left-open right-closed interval $(a, b]$. In other words, $[a, b] \setminus \{a\} = (a, b]$.

Set.Icc_diff_right theorem

: Icc a b \ { b } = Ico a b

Full source

@[simp]
theorem Icc_diff_right : IccIcc a b \ {b} = Ico a b :=
  ext fun x => by simp [lt_iff_le_and_ne, and_assoc]

Difference of Closed Interval and Right Endpoint Equals Left-Closed Right-Open Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the difference between the closed interval $[a, b]$ and the singleton set $\{b\}$ is equal to the left-closed right-open interval $[a, b)$. In other words, $[a, b] \setminus \{b\} = [a, b)$.

Set.Ico_diff_left theorem

: Ico a b \ { a } = Ioo a b

Full source

@[simp]
theorem Ico_diff_left : IcoIco a b \ {a} = Ioo a b :=
  ext fun x => by simp [and_right_comm, ← lt_iff_le_and_ne, eq_comm]

Difference of Left-Closed Right-Open Interval and Left Endpoint Equals Open Interval

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, the set difference between the left-closed right-open interval $[a, b)$ and the singleton set $\{a\}$ is equal to the open interval $(a, b)$. In other words, $[a, b) \setminus \{a\} = (a, b)$.

Set.Ioc_diff_right theorem

: Ioc a b \ { b } = Ioo a b

Full source

@[simp]
theorem Ioc_diff_right : IocIoc a b \ {b} = Ioo a b :=
  ext fun x => by simp [and_assoc, ← lt_iff_le_and_ne]

Difference of Right-Closed Interval and Right Endpoint Equals Open Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the set difference between the left-open right-closed interval $(a, b]$ and the singleton set $\{b\}$ equals the open interval $(a, b)$. In other words, $(a, b] \setminus \{b\} = (a, b)$.

Set.Icc_diff_both theorem

: Icc a b \ { a, b } = Ioo a b

Full source

@[simp]
theorem Icc_diff_both : IccIcc a b \ {a, b} = Ioo a b := by
  rw [insert_eq, ← diff_diff, Icc_diff_left, Ioc_diff_right]

Difference of Closed Interval and Endpoints Equals Open Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the set difference between the closed interval $[a, b]$ and the set $\{a, b\}$ is equal to the open interval $(a, b)$. In other words, $[a, b] \setminus \{a, b\} = (a, b)$.

Set.Ici_diff_left theorem

: Ici a \ { a } = Ioi a

Full source

@[simp]
theorem Ici_diff_left : IciIci a \ {a} = Ioi a :=
  ext fun x => by simp [lt_iff_le_and_ne, eq_comm]

Difference between $[a, \infty)$ and $\{a\}$ is $(a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the difference between the left-closed right-infinite interval $[a, \infty)$ and the singleton set $\{a\}$ is equal to the left-open right-infinite interval $(a, \infty)$. In other words, $[a, \infty) \setminus \{a\} = (a, \infty)$.

Set.Iic_diff_right theorem

: Iic a \ { a } = Iio a

Full source

@[simp]
theorem Iic_diff_right : IicIic a \ {a} = Iio a :=
  ext fun x => by simp [lt_iff_le_and_ne]

Difference between $(-\infty, a]$ and $\{a\}$ is $(-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$, the difference between the left-infinite right-closed interval $(-\infty, a]$ and the singleton set $\{a\}$ is equal to the left-infinite right-open interval $(-\infty, a)$. In other words, $(-\infty, a] \setminus \{a\} = (-\infty, a)$.

Set.Ico_diff_Ioo_same theorem

(h : a < b) : Ico a b \ Ioo a b = { a }

Full source

@[simp]
theorem Ico_diff_Ioo_same (h : a < b) : IcoIco a b \ Ioo a b = {a} := by
  rw [← Ico_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Ico.2 h)]

Difference of $[a, b)$ and $(a, b)$ is $\{a\}$ when $a < b$

Informal description

For any two elements $a$ and $b$ in a preorder with $a < b$, the set difference between the left-closed right-open interval $[a, b)$ and the open interval $(a, b)$ is the singleton set $\{a\}$. In other words, $[a, b) \setminus (a, b) = \{a\}$.

Set.Ioc_diff_Ioo_same theorem

(h : a < b) : Ioc a b \ Ioo a b = { b }

Full source

@[simp]
theorem Ioc_diff_Ioo_same (h : a < b) : IocIoc a b \ Ioo a b = {b} := by
  rw [← Ioc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Ioc.2 h)]

Difference of $(a, b]$ and $(a, b)$ is $\{b\}$ when $a < b$

Informal description

For any elements $a$ and $b$ in a preorder with $a < b$, the set difference between the left-open right-closed interval $(a, b]$ and the open interval $(a, b)$ is the singleton set $\{b\}$. In other words, $(a, b] \setminus (a, b) = \{b\}$.

Set.Icc_diff_Ico_same theorem

(h : a ≤ b) : Icc a b \ Ico a b = { b }

Full source

@[simp]
theorem Icc_diff_Ico_same (h : a ≤ b) : IccIcc a b \ Ico a b = {b} := by
  rw [← Icc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Icc.2 h)]

Difference of Closed and Left-Closed Right-Open Intervals at Right Endpoint

Informal description

For any elements $a$ and $b$ in a preorder with $a \leq b$, the set difference between the closed interval $[a, b]$ and the left-closed right-open interval $[a, b)$ is the singleton set $\{b\}$. In other words, $[a, b] \setminus [a, b) = \{b\}$.

Set.Icc_diff_Ioc_same theorem

(h : a ≤ b) : Icc a b \ Ioc a b = { a }

Full source

@[simp]
theorem Icc_diff_Ioc_same (h : a ≤ b) : IccIcc a b \ Ioc a b = {a} := by
  rw [← Icc_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Icc.2 h)]

Difference of Closed and Left-Open Right-Closed Intervals at Left Endpoint: $[a, b] \setminus (a, b] = \{a\}$

Informal description

For any elements $a$ and $b$ in a preorder with $a \leq b$, the set difference between the closed interval $[a, b]$ and the left-open right-closed interval $(a, b]$ is the singleton set $\{a\}$. In other words, $[a, b] \setminus (a, b] = \{a\}$.

Set.Icc_diff_Ioo_same theorem

(h : a ≤ b) : Icc a b \ Ioo a b = { a, b }

Full source

@[simp]
theorem Icc_diff_Ioo_same (h : a ≤ b) : IccIcc a b \ Ioo a b = {a, b} := by
  rw [← Icc_diff_both, diff_diff_cancel_left]
  simp [insert_subset_iff, h]

Difference of Closed and Open Intervals Yields Endpoints: $[a, b] \setminus (a, b) = \{a, b\}$

Informal description

For any elements $a$ and $b$ in a preorder with $a \leq b$, the set difference between the closed interval $[a, b]$ and the open interval $(a, b)$ is the set $\{a, b\}$. In other words, $[a, b] \setminus (a, b) = \{a, b\}$.

Set.Ici_diff_Ioi_same theorem

: Ici a \ Ioi a = { a }

Full source

@[simp]
theorem Ici_diff_Ioi_same : IciIci a \ Ioi a = {a} := by
  rw [← Ici_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 left_mem_Ici)]

Difference of Closed and Open Right-Infinite Intervals Yields Singleton

Informal description

For any element $a$ in a preorder $\alpha$, the difference between the left-closed right-infinite interval $[a, \infty)$ and the left-open right-infinite interval $(a, \infty)$ is the singleton set $\{a\}$. In other words, $[a, \infty) \setminus (a, \infty) = \{a\}$.

Set.Iic_diff_Iio_same theorem

: Iic a \ Iio a = { a }

Full source

@[simp]
theorem Iic_diff_Iio_same : IicIic a \ Iio a = {a} := by
  rw [← Iic_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 right_mem_Iic)]

Difference of Closed and Open Left-Infinite Intervals Yields Singleton

Informal description

For any element $a$ in a preorder $\alpha$, the difference between the left-infinite right-closed interval $(-\infty, a]$ and the left-infinite right-open interval $(-\infty, a)$ is the singleton set $\{a\}$. In other words, $(-\infty, a] \setminus (-\infty, a) = \{a\}$.

Set.Ioi_union_left theorem

: Ioi a ∪ { a } = Ici a

Full source

theorem Ioi_union_left : IoiIoi a ∪ {a} = Ici a :=
  ext fun x => by simp [eq_comm, le_iff_eq_or_lt]

Union of Left-Open Interval and Singleton Equals Left-Closed Interval

Informal description

For any element $a$ in a preorder $\alpha$, the union of the left-open right-infinite interval $(a, \infty)$ and the singleton set $\{a\}$ equals the left-closed right-infinite interval $[a, \infty)$. That is, $(a, \infty) \cup \{a\} = [a, \infty)$.

Set.Iio_union_right theorem

: Iio a ∪ { a } = Iic a

Full source

theorem Iio_union_right : IioIio a ∪ {a} = Iic a :=
  ext fun _ => le_iff_lt_or_eq.symm

Union of Left-Open Interval and Singleton Equals Left-Closed Interval

Informal description

For any element $a$ in a preorder $\alpha$, the union of the left-infinite right-open interval $(-\infty, a)$ and the singleton set $\{a\}$ equals the left-infinite right-closed interval $(-\infty, a]$, i.e., $(-\infty, a) \cup \{a\} = (-\infty, a]$.

Set.Ioo_union_left theorem

(hab : a < b) : Ioo a b ∪ { a } = Ico a b

Full source

theorem Ioo_union_left (hab : a < b) : IooIoo a b ∪ {a} = Ico a b := by
  rw [← Ico_diff_left, diff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]

Union of Open Interval and Left Endpoint Equals Left-Closed Right-Open Interval

Informal description

For any two elements $a$ and $b$ in a preorder with $a < b$, the union of the open interval $(a, b)$ and the singleton $\{a\}$ equals the left-closed right-open interval $[a, b)$. That is, $(a, b) \cup \{a\} = [a, b)$.

Set.Ioo_union_right theorem

(hab : a < b) : Ioo a b ∪ { b } = Ioc a b

Full source

theorem Ioo_union_right (hab : a < b) : IooIoo a b ∪ {b} = Ioc a b := by
  simpa only [Ioo_toDual, Ico_toDual] using Ioo_union_left hab.dual

Union of Open Interval and Right Endpoint Equals Left-Open Right-Closed Interval

Informal description

For any two elements $a$ and $b$ in a preorder with $a < b$, the union of the open interval $(a, b)$ and the singleton $\{b\}$ equals the left-open right-closed interval $(a, b]$. That is, $(a, b) \cup \{b\} = (a, b]$.

Set.Ioo_union_both theorem

(h : a ≤ b) : Ioo a b ∪ { a, b } = Icc a b

Full source

theorem Ioo_union_both (h : a ≤ b) : IooIoo a b ∪ {a, b} = Icc a b := by
  have : (Icc a b \ {a, b}) ∪ {a, b} = Icc a b := diff_union_of_subset fun
    | x, .inl rfl => left_mem_Icc.mpr h
    | x, .inr rfl => right_mem_Icc.mpr h
  rw [← this, Icc_diff_both]

Union of Open Interval and Endpoints Equals Closed Interval when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder with $a \leq b$, the union of the open interval $(a, b)$ and the set $\{a, b\}$ equals the closed interval $[a, b]$. That is, $(a, b) \cup \{a, b\} = [a, b]$.

Set.Ioc_union_left theorem

(hab : a ≤ b) : Ioc a b ∪ { a } = Icc a b

Full source

theorem Ioc_union_left (hab : a ≤ b) : IocIoc a b ∪ {a} = Icc a b := by
  rw [← Icc_diff_left, diff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)]

Union of $(a, b]$ and $\{a\}$ equals $[a, b]$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the union of the left-open right-closed interval $(a, b]$ and the singleton $\{a\}$ equals the closed interval $[a, b]$. That is, $(a, b] \cup \{a\} = [a, b]$.

Set.Ico_union_right theorem

(hab : a ≤ b) : Ico a b ∪ { b } = Icc a b

Full source

theorem Ico_union_right (hab : a ≤ b) : IcoIco a b ∪ {b} = Icc a b := by
  simpa only [Ioc_toDual, Icc_toDual] using Ioc_union_left hab.dual

Union of $[a, b)$ and $\{b\}$ equals $[a, b]$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the union of the left-closed right-open interval $[a, b)$ and the singleton $\{b\}$ equals the closed interval $[a, b]$. That is, $[a, b) \cup \{b\} = [a, b]$.

Set.Ico_insert_right theorem

(h : a ≤ b) : insert b (Ico a b) = Icc a b

Full source

@[simp]
theorem Ico_insert_right (h : a ≤ b) : insert b (Ico a b) = Icc a b := by
  rw [insert_eq, union_comm, Ico_union_right h]

Insertion of Right Endpoint into $[a, b)$ Yields $[a, b]$ When $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, inserting $b$ into the left-closed right-open interval $[a, b)$ yields the closed interval $[a, b]$. That is, $\{b\} \cup [a, b) = [a, b]$.

Set.Ioc_insert_left theorem

(h : a ≤ b) : insert a (Ioc a b) = Icc a b

Full source

@[simp]
theorem Ioc_insert_left (h : a ≤ b) : insert a (Ioc a b) = Icc a b := by
  rw [insert_eq, union_comm, Ioc_union_left h]

Insertion of Left Endpoint into $(a, b]$ Yields $[a, b]$ When $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the insertion of $a$ into the left-open right-closed interval $(a, b]$ equals the closed interval $[a, b]$. That is, $\{a\} \cup (a, b] = [a, b]$.

Set.Ioo_insert_left theorem

(h : a < b) : insert a (Ioo a b) = Ico a b

Full source

@[simp]
theorem Ioo_insert_left (h : a < b) : insert a (Ioo a b) = Ico a b := by
  rw [insert_eq, union_comm, Ioo_union_left h]

Insertion of Left Endpoint into Open Interval Yields Left-Closed Right-Open Interval

Informal description

For any two elements $a$ and $b$ in a preorder with $a < b$, inserting $a$ into the open interval $(a, b)$ yields the left-closed right-open interval $[a, b)$. That is, $\{a\} \cup (a, b) = [a, b)$.

Set.Ioo_insert_right theorem

(h : a < b) : insert b (Ioo a b) = Ioc a b

Full source

@[simp]
theorem Ioo_insert_right (h : a < b) : insert b (Ioo a b) = Ioc a b := by
  rw [insert_eq, union_comm, Ioo_union_right h]

Union of Open Interval and Right Endpoint Equals Left-Open Right-Closed Interval

Informal description

For any two elements $a$ and $b$ in a preorder with $a < b$, the union of the open interval $(a, b)$ and the singleton $\{b\}$ equals the left-open right-closed interval $(a, b]$. That is, $(a, b) \cup \{b\} = (a, b]$.

Set.Iio_insert theorem

: insert a (Iio a) = Iic a

Full source

@[simp]
theorem Iio_insert : insert a (Iio a) = Iic a :=
  ext fun _ => le_iff_eq_or_lt.symm

Insertion into Left-Open Interval Yields Left-Closed Interval

Informal description

For any element $a$ in a preorder $\alpha$, inserting $a$ into the left-infinite right-open interval $(-\infty, a)$ yields the left-infinite right-closed interval $(-\infty, a]$, i.e., $\{a\} \cup (-\infty, a) = (-\infty, a]$.

Set.Ioi_insert theorem

: insert a (Ioi a) = Ici a

Full source

@[simp]
theorem Ioi_insert : insert a (Ioi a) = Ici a :=
  ext fun _ => (or_congr_left eq_comm).trans le_iff_eq_or_lt.symm

Insertion of Point into Open Interval Yields Closed Interval

Informal description

For any element $a$ in a preorder $\alpha$, the union of the singleton set $\{a\}$ and the left-open right-infinite interval $(a, \infty)$ equals the left-closed right-infinite interval $[a, \infty)$. In other words, $\{a\} \cup (a, \infty) = [a, \infty)$.

Set.mem_Ici_Ioi_of_subset_of_subset theorem

{s : Set α} (ho : Ioi a ⊆ s) (hc : s ⊆ Ici a) : s ∈ ({Ici a, Ioi a} : Set (Set α))

Full source

theorem mem_Ici_Ioi_of_subset_of_subset {s : Set α} (ho : IoiIoi a ⊆ s) (hc : s ⊆ Ici a) :
    s ∈ ({Ici a, Ioi a} : Set (Set α)) :=
  by_cases
    (fun h : a ∈ s =>
      Or.inl <| Subset.antisymm hc <| by rw [← Ioi_union_left, union_subset_iff]; simp [*])
    fun h =>
    Or.inr <| Subset.antisymm (fun _ hx => lt_of_le_of_ne (hc hx) fun heq => h <| heq.symm ▸ hx) ho

Characterization of subsets between $(a, \infty)$ and $[a, \infty)$

Informal description

For any subset $s$ of a preorder $\alpha$, if the left-open right-infinite interval $(a, \infty)$ is contained in $s$ and $s$ is contained in the left-closed right-infinite interval $[a, \infty)$, then $s$ must be equal to either $[a, \infty)$ or $(a, \infty)$.

Set.mem_Iic_Iio_of_subset_of_subset theorem

{s : Set α} (ho : Iio a ⊆ s) (hc : s ⊆ Iic a) : s ∈ ({Iic a, Iio a} : Set (Set α))

Full source

theorem mem_Iic_Iio_of_subset_of_subset {s : Set α} (ho : IioIio a ⊆ s) (hc : s ⊆ Iic a) :
    s ∈ ({Iic a, Iio a} : Set (Set α)) :=
  @mem_Ici_Ioi_of_subset_of_subset αᵒᵈ _ a s ho hc

Characterization of subsets between $(-\infty, a)$ and $(-\infty, a]$

Informal description

For any subset $s$ of a preorder $\alpha$, if the left-infinite right-open interval $(-\infty, a)$ is contained in $s$ and $s$ is contained in the left-infinite right-closed interval $(-\infty, a]$, then $s$ must be equal to either $(-\infty, a]$ or $(-\infty, a)$.

Set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset theorem

{s : Set α} (ho : Ioo a b ⊆ s) (hc : s ⊆ Icc a b) : s ∈ ({Icc a b, Ico a b, Ioc a b, Ioo a b} : Set (Set α))

Full source

theorem mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {s : Set α} (ho : IooIoo a b ⊆ s) (hc : s ⊆ Icc a b) :
    s ∈ ({Icc a b, Ico a b, Ioc a b, Ioo a b} : Set (Set α)) := by
  classical
    by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
    · refine Or.inl (Subset.antisymm hc ?_)
      rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right,
        diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_right]
        exact subset_diff_singleton hc hb
      · rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
    · refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_left]
        exact subset_diff_singleton hc ha
      · rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho
      rw [← Ico_diff_left, ← Icc_diff_right]
      apply_rules [subset_diff_singleton]

Characterization of subsets between $(a, b)$ and $[a, b]$

Informal description

For any subset $s$ of a preorder $\alpha$, if the open interval $(a, b)$ is contained in $s$ and $s$ is contained in the closed interval $[a, b]$, then $s$ must be one of the four intervals: $[a, b]$, $[a, b)$, $(a, b]$, or $(a, b)$.

IsMax.Ici_eq theorem

(h : IsMax a) : Ici a = { a }

Full source

theorem _root_.IsMax.Ici_eq (h : IsMax a) : Ici a = {a} :=
  eq_singleton_iff_unique_mem.2 ⟨left_mem_Ici, fun _ => h.eq_of_ge⟩

Maximal Element Characterizes Singleton Interval: $[a, \infty) = \{a\}$ for Maximal $a$

Informal description

If $a$ is a maximal element in a preorder $\alpha$, then the left-closed right-infinite interval $[a, \infty)$ is equal to the singleton set $\{a\}$.

IsMin.Iic_eq theorem

(h : IsMin a) : Iic a = { a }

Full source

theorem _root_.IsMin.Iic_eq (h : IsMin a) : Iic a = {a} :=
  h.toDual.Ici_eq

Minimal Element Characterizes Singleton Interval: $(-\infty, a] = \{a\}$ for Minimal $a$

Informal description

If $a$ is a minimal element in a preorder $\alpha$, then the left-infinite right-closed interval $(-\infty, a]$ is equal to the singleton set $\{a\}$.

Set.Ici_injective theorem

: Injective (Ici : α → Set α)

Full source

theorem Ici_injective : Injective (Ici : α → Set α) := fun _ _ =>
  eq_of_forall_ge_iffeq_of_forall_ge_iff ∘ Set.ext_iff.1

Injectivity of the Left-Closed Right-Infinite Interval Function

Informal description

The function that maps each element $a$ in a preorder $\alpha$ to the left-closed right-infinite interval $[a, \infty)$ is injective. In other words, for any two elements $a, b \in \alpha$, if $[a, \infty) = [b, \infty)$, then $a = b$.

Set.Iic_injective theorem

: Injective (Iic : α → Set α)

Full source

theorem Iic_injective : Injective (Iic : α → Set α) := fun _ _ =>
  eq_of_forall_le_iffeq_of_forall_le_iff ∘ Set.ext_iff.1

Injectivity of the Left-Infinite Right-Closed Interval Function

Informal description

The function that maps each element $a$ in a preorder $\alpha$ to the left-infinite right-closed interval $(-\infty, a]$ is injective. In other words, if $(-\infty, a] = (-\infty, b]$, then $a = b$.

Set.Ici_inj theorem

: Ici a = Ici b ↔ a = b

Full source

theorem Ici_inj : IciIci a = Ici b ↔ a = b :=
  Ici_injective.eq_iff

Equality of Left-Closed Right-Infinite Intervals is Equivalent to Equality of Endpoints

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the equality of the left-closed right-infinite intervals $[a, \infty) = [b, \infty)$ holds if and only if $a = b$.

Set.Iic_inj theorem

: Iic a = Iic b ↔ a = b

Full source

theorem Iic_inj : IicIic a = Iic b ↔ a = b :=
  Iic_injective.eq_iff

Equality of Left-Infinite Right-Closed Intervals is Equivalent to Equality of Endpoints

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the equality of the left-infinite right-closed intervals $(-\infty, a] = (-\infty, b]$ holds if and only if $a = b$.

Set.Icc_inter_Icc_eq_singleton theorem

(hab : a ≤ b) (hbc : b ≤ c) : Icc a b ∩ Icc b c = { b }

Full source

@[simp]
theorem Icc_inter_Icc_eq_singleton (hab : a ≤ b) (hbc : b ≤ c) : IccIcc a b ∩ Icc b c = {b} := by
  rw [← Ici_inter_Iic, ← Iic_inter_Ici, inter_inter_inter_comm, Iic_inter_Ici]
  simp [hab, hbc]

Intersection of Adjacent Closed Intervals is Singleton: $[a, b] \cap [b, c] = \{b\}$

Informal description

For any elements $a$, $b$, and $c$ in a preorder $\alpha$ such that $a \leq b$ and $b \leq c$, the intersection of the closed intervals $[a, b]$ and $[b, c]$ is the singleton set $\{b\}$, i.e., $$ [a, b] \cap [b, c] = \{b\}. $$

Set.Icc_eq_Icc_iff theorem

{d : α} (h : a ≤ b) : Icc a b = Icc c d ↔ a = c ∧ b = d

Full source

lemma Icc_eq_Icc_iff {d : α} (h : a ≤ b) :
    IccIcc a b = Icc c d ↔ a = c ∧ b = d := by
  refine ⟨fun heq ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  have h' : c ≤ d := by
    by_contra contra; rw [Icc_eq_empty_iff.mpr contra, Icc_eq_empty_iff] at heq; contradiction
  simp only [Set.ext_iff, mem_Icc] at heq
  obtain ⟨-, h₁⟩ := (heq b).mp ⟨h, le_refl _⟩
  obtain ⟨h₂, -⟩ := (heq a).mp ⟨le_refl _, h⟩
  obtain ⟨h₃, -⟩ := (heq c).mpr ⟨le_refl _, h'⟩
  obtain ⟨-, h₄⟩ := (heq d).mpr ⟨h', le_refl _⟩
  exact ⟨le_antisymm h₃ h₂, le_antisymm h₁ h₄⟩

Equality of Closed Intervals: $[a, b] = [c, d] \leftrightarrow a = c \land b = d$

Informal description

For any elements $a, b, c, d$ in a preorder $\alpha$ with $a \leq b$, the closed intervals $[a, b]$ and $[c, d]$ are equal if and only if $a = c$ and $b = d$.

Set.Ici_top theorem

[PartialOrder α] [OrderTop α] : Ici (⊤ : α) = {⊤}

Full source

@[simp]
theorem Ici_top [PartialOrder α] [OrderTop α] : Ici (⊤ : α) = {⊤} :=
  isMax_top.Ici_eq

Singleton Interval at Top: $[\top, \infty) = \{\top\}$

Informal description

In a partially ordered set $\alpha$ with a greatest element $\top$, the left-closed right-infinite interval $[\top, \infty)$ is equal to the singleton set $\{\top\}$.

Set.Ioi_top theorem

: Ioi (⊤ : α) = ∅

Full source

theorem Ioi_top : Ioi (⊤ : α) = ∅ :=
  isMax_top.Ioi_eq

Emptyness of Strict Upper Interval Above Top Element: $(\top, \infty) = \emptyset$

Informal description

For any type $\alpha$ with a partial order and a greatest element $\top$, the left-open right-infinite interval $(\top, \infty)$ is empty.

Set.Iic_top theorem

: Iic (⊤ : α) = univ

Full source

@[simp]
theorem Iic_top : Iic (⊤ : α) = univ :=
  isTop_top.Iic_eq

Interval Characterization of Top Element: $(-\infty, \top] = \alpha$

Informal description

For any type $\alpha$ with a partial order and a greatest element $\top$, the left-infinite right-closed interval $(-\infty, \top]$ is equal to the entire set $\alpha$.

Set.Icc_top theorem

: Icc a ⊤ = Ici a

Full source

@[simp]
theorem Icc_top : Icc a ⊤ = Ici a := by simp [← Ici_inter_Iic]

Closed Interval with Top Equals Left-Closed Right-Infinite Interval

Informal description

For any element $a$ in a partially ordered set $\alpha$ with a greatest element $\top$, the closed interval $[a, \top]$ is equal to the left-closed right-infinite interval $[a, \infty)$.

Set.Ioc_top theorem

: Ioc a ⊤ = Ioi a

Full source

@[simp]
theorem Ioc_top : Ioc a ⊤ = Ioi a := by simp [← Ioi_inter_Iic]

Equality of Intervals: $(a, \top] = (a, \infty)$ in an Order with Top Element

Informal description

For any element $a$ in a preorder $\alpha$ with a greatest element $\top$, the left-open right-closed interval $(a, \top]$ is equal to the left-open right-infinite interval $(a, \infty)$.

Set.Iic_bot theorem

[PartialOrder α] [OrderBot α] : Iic (⊥ : α) = {⊥}

Full source

@[simp]
theorem Iic_bot [PartialOrder α] [OrderBot α] : Iic (⊥ : α) = {⊥} :=
  isMin_bot.Iic_eq

Bottom Interval is Singleton: $(-\infty, \bot] = \{\bot\}$

Informal description

In a partially ordered set $\alpha$ with a bottom element $\bot$, the left-infinite right-closed interval $(-\infty, \bot]$ is equal to the singleton set $\{\bot\}$.

Set.Iio_bot theorem

: Iio (⊥ : α) = ∅

Full source

theorem Iio_bot : Iio (⊥ : α) = ∅ :=
  isMin_bot.Iio_eq

Empty Interval Below Bottom Element: $(-\infty, \bot) = \emptyset$

Informal description

In an ordered type $\alpha$ with a bottom element $\bot$, the left-infinite right-open interval $(-\infty, \bot)$ is empty, i.e., $\{x \mid x < \bot\} = \emptyset$.

Set.Ici_bot theorem

: Ici (⊥ : α) = univ

Full source

@[simp]
theorem Ici_bot : Ici (⊥ : α) = univ :=
  isBot_bot.Ici_eq

Bottom Element Makes Closed-Infinite Interval Universal

Informal description

In an ordered type $\alpha$ with a bottom element $\bot$, the left-closed right-infinite interval $[\bot, \infty)$ is equal to the entire set $\alpha$.

Set.Icc_bot theorem

: Icc ⊥ a = Iic a

Full source

@[simp]
theorem Icc_bot : Icc ⊥ a = Iic a := by simp [← Ici_inter_Iic]

Closed Interval from Bottom Equals Left-Infinite Closed Interval

Informal description

In an ordered type $\alpha$ with a bottom element $\bot$, the closed interval $[\bot, a]$ is equal to the left-infinite right-closed interval $(-\infty, a]$.

Set.Ico_bot theorem

: Ico ⊥ a = Iio a

Full source

@[simp]
theorem Ico_bot : Ico ⊥ a = Iio a := by simp [← Ici_inter_Iio]

Equality of Bottom-Based Interval and Strictly Below Interval: $[\bot, a) = (-\infty, a)$

Informal description

In an ordered type $\alpha$ with a bottom element $\bot$, the left-closed right-open interval $[\bot, a)$ is equal to the left-infinite right-open interval $(-\infty, a)$ for any element $a \in \alpha$.

Set.Icc_bot_top theorem

[Preorder α] [BoundedOrder α] : Icc (⊥ : α) ⊤ = univ

Full source

theorem Icc_bot_top [Preorder α] [BoundedOrder α] : Icc (⊥ : α) ⊤ = univ := by simp

Closed Interval from Bottom to Top Equals Universe

Informal description

In a preorder $\alpha$ with both a least element $\bot$ and a greatest element $\top$, the closed interval $[\bot, \top]$ is equal to the entire set $\alpha$.

Set.Iic_inter_Iic theorem

{a b : α} : Iic a ∩ Iic b = Iic (a ⊓ b)

Full source

@[simp]
theorem Iic_inter_Iic {a b : α} : IicIic a ∩ Iic b = Iic (a ⊓ b) := by
  ext x
  simp [Iic]

Intersection of Left-Infinite Right-Closed Intervals Equals Interval of Infimum

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the intersection of the left-infinite right-closed intervals $(-\infty, a]$ and $(-\infty, b]$ is equal to the left-infinite right-closed interval $(-\infty, a \sqcap b]$, where $\sqcap$ denotes the infimum (greatest lower bound) of $a$ and $b$.

Set.Ioc_inter_Iic theorem

(a b c : α) : Ioc a b ∩ Iic c = Ioc a (b ⊓ c)

Full source

@[simp]
theorem Ioc_inter_Iic (a b c : α) : IocIoc a b ∩ Iic c = Ioc a (b ⊓ c) := by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]

Intersection of $(a, b]$ and $(-\infty, c]$ is $(a, b \sqcap c]$

Informal description

For any elements $a$, $b$, and $c$ in a preorder $\alpha$, the intersection of the left-open right-closed interval $(a, b]$ and the left-infinite right-closed interval $(-\infty, c]$ is equal to the left-open right-closed interval $(a, b \sqcap c]$, where $\sqcap$ denotes the infimum of $b$ and $c$. In symbols: $$ (a, b] \cap (-\infty, c] = (a, b \sqcap c] $$

Set.Ici_inter_Ici theorem

{a b : α} : Ici a ∩ Ici b = Ici (a ⊔ b)

Full source

@[simp]
theorem Ici_inter_Ici {a b : α} : IciIci a ∩ Ici b = Ici (a ⊔ b) := by
  ext x
  simp [Ici]

Intersection of Right-Infinite Closed Intervals Equals Supremum Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the intersection of the left-closed right-infinite intervals $[a, \infty)$ and $[b, \infty)$ is equal to the left-closed right-infinite interval $[a \sqcup b, \infty)$, where $\sqcup$ denotes the supremum (least upper bound) of $a$ and $b$.

Set.Ico_inter_Ici theorem

(a b c : α) : Ico a b ∩ Ici c = Ico (a ⊔ c) b

Full source

@[simp]
theorem Ico_inter_Ici (a b c : α) : IcoIco a b ∩ Ici c = Ico (a ⊔ c) b := by
  rw [← Ici_inter_Iio, ← Ici_inter_Iio, ← Ici_inter_Ici, inter_right_comm]

Intersection of $[a, b)$ and $[c, \infty)$ is $[a \sqcup c, b)$

Informal description

For any elements $a$, $b$, and $c$ in a preorder $\alpha$, the intersection of the left-closed right-open interval $[a, b)$ and the left-closed right-infinite interval $[c, \infty)$ is equal to the left-closed right-open interval $[a \sqcup c, b)$, where $\sqcup$ denotes the supremum of $a$ and $c$.

Set.Icc_inter_Icc theorem

: Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Full source

theorem Icc_inter_Icc : IccIcc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂) := by
  simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]; ac_rfl

Intersection of Closed Intervals Equals Interval of Suprema and Infima

Informal description

For any elements $a_1, b_1, a_2, b_2$ in a preorder $\alpha$, the intersection of the closed intervals $[a_1, b_1]$ and $[a_2, b_2]$ is equal to the closed interval $[a_1 \sqcup a_2, b_1 \sqcap b_2]$, where $\sqcup$ denotes the supremum and $\sqcap$ denotes the infimum.

Set.Iic_prod_Iic theorem

(a : α) (b : β) : Iic a ×ˢ Iic b = Iic (a, b)

Full source

@[simp]
theorem Iic_prod_Iic (a : α) (b : β) : Iic a ×ˢ Iic b = Iic (a, b) :=
  rfl

Product of Left-Infinite Right-Closed Intervals in Product Order

Informal description

For any elements $a$ in a preorder $\alpha$ and $b$ in a preorder $\beta$, the product of the left-infinite right-closed intervals $(-\infty, a] \subseteq \alpha$ and $(-\infty, b] \subseteq \beta$ is equal to the left-infinite right-closed interval $(-\infty, (a, b)]$ in the product order $\alpha \times \beta$. That is, $$ (-\infty, a] \times (-\infty, b] = (-\infty, (a, b)]. $$

Set.Ici_prod_Ici theorem

(a : α) (b : β) : Ici a ×ˢ Ici b = Ici (a, b)

Full source

@[simp]
theorem Ici_prod_Ici (a : α) (b : β) : Ici a ×ˢ Ici b = Ici (a, b) :=
  rfl

Product of Right-Infinite Closed Intervals Equals Right-Infinite Closed Interval in Product Space

Informal description

For any elements $a$ in a preorder $\alpha$ and $b$ in a preorder $\beta$, the product of the intervals $[a, \infty)$ in $\alpha$ and $[b, \infty)$ in $\beta$ is equal to the interval $[(a, b), \infty)$ in the product preorder $\alpha \times \beta$. In other words, $$ [a, \infty) \times [b, \infty) = [(a, b), \infty). $$

Set.Ici_prod_eq theorem

(a : α × β) : Ici a = Ici a.1 ×ˢ Ici a.2

Full source

theorem Ici_prod_eq (a : α × β) : Ici a = Ici a.1 ×ˢ Ici a.2 :=
  rfl

Product Interval Decomposition: $[a, \infty) = [a_1, \infty) \times [a_2, \infty)$ for $a = (a_1, a_2)$

Informal description

For any element $a = (a_1, a_2)$ in the product type $\alpha \times \beta$, the left-closed right-infinite interval $[a, \infty)$ in the product order is equal to the Cartesian product of the left-closed right-infinite intervals $[a_1, \infty) \times [a_2, \infty)$.

Set.Iic_prod_eq theorem

(a : α × β) : Iic a = Iic a.1 ×ˢ Iic a.2

Full source

theorem Iic_prod_eq (a : α × β) : Iic a = Iic a.1 ×ˢ Iic a.2 :=
  rfl

Product Interval Decomposition: $(-\infty, (a_1, a_2)] = (-\infty, a_1] \times (-\infty, a_2]$

Informal description

For any element $a = (a_1, a_2)$ in the product preorder $\alpha \times \beta$, the left-infinite right-closed interval $(-\infty, a]$ is equal to the Cartesian product of the left-infinite right-closed intervals $(-\infty, a_1] \times (-\infty, a_2]$.

Set.Icc_prod_Icc theorem

(a₁ a₂ : α) (b₁ b₂ : β) : Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)

Full source

@[simp]
theorem Icc_prod_Icc (a₁ a₂ : α) (b₁ b₂ : β) : Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂) := by
  ext ⟨x, y⟩
  simp [and_assoc, and_comm, and_left_comm]

Product of Closed Intervals Equals Closed Interval in Product Order

Informal description

For any elements $a_1, a_2$ in a preorder $\alpha$ and $b_1, b_2$ in a preorder $\beta$, the product of the closed intervals $[a_1, a_2] \times [b_1, b_2]$ is equal to the closed interval $[(a_1, b_1), (a_2, b_2)]$ in the product order on $\alpha \times \beta$.

Set.Icc_prod_eq theorem

(a b : α × β) : Icc a b = Icc a.1 b.1 ×ˢ Icc a.2 b.2

Full source

theorem Icc_prod_eq (a b : α × β) : Icc a b = Icc a.1 b.1 ×ˢ Icc a.2 b.2 := by simp

Product Interval Decomposition: $[a, b] = [a_1, b_1] \times [a_2, b_2]$

Informal description

For any elements $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in the product preorder $\alpha \times \beta$, the closed interval $[a, b]$ is equal to the Cartesian product of the closed intervals $[a_1, b_1] \times [a_2, b_2]$.

instNoMinOrderElemIoo instance

: NoMinOrder (Set.Ioo x y)

Full source

instance : NoMinOrder (Set.Ioo x y) :=
  ⟨fun ⟨a, ha₁, ha₂⟩ => by
    rcases exists_between ha₁ with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, hb₁, hb₂.trans ha₂⟩, hb₂⟩⟩

Open Intervals Have No Minimal Elements

Informal description

For any two elements $x$ and $y$ in a preorder $\alpha$, the open interval $(x, y)$ has no minimal elements. That is, for every element $a$ in $(x, y)$, there exists another element $b$ in $(x, y)$ such that $b < a$.

instNoMinOrderElemIoc instance

: NoMinOrder (Set.Ioc x y)

Full source

instance : NoMinOrder (Set.Ioc x y) :=
  ⟨fun ⟨a, ha₁, ha₂⟩ => by
    rcases exists_between ha₁ with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, hb₁, hb₂.le.trans ha₂⟩, hb₂⟩⟩

No Minimal Element in Left-Open Right-Closed Interval

Informal description

For any two elements $x$ and $y$ in a preorder $\alpha$, the left-open right-closed interval $(x, y]$ has no minimal element. That is, for every element $a$ in $(x, y]$, there exists another element $b$ in $(x, y]$ such that $b < a$.

instNoMinOrderElemIoi instance

: NoMinOrder (Set.Ioi x)

Full source

instance : NoMinOrder (Set.Ioi x) :=
  ⟨fun ⟨a, ha⟩ => by
    rcases exists_between ha with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, hb₁⟩, hb₂⟩⟩

No Minimal Element in Left-Open Right-Infinite Interval

Informal description

For any element $x$ in a preorder $\alpha$, the left-open right-infinite interval $(x, \infty)$ has no minimal element.

instNoMaxOrderElemIoo instance

: NoMaxOrder (Set.Ioo x y)

Full source

instance : NoMaxOrder (Set.Ioo x y) :=
  ⟨fun ⟨a, ha₁, ha₂⟩ => by
    rcases exists_between ha₂ with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, ha₁.trans hb₁, hb₂⟩, hb₁⟩⟩

No Maximal Element in Open Intervals

Informal description

For any two elements $x$ and $y$ in a preorder $\alpha$, the open interval $(x, y)$ has no maximal element.

instNoMaxOrderElemIco instance

: NoMaxOrder (Set.Ico x y)

Full source

instance : NoMaxOrder (Set.Ico x y) :=
  ⟨fun ⟨a, ha₁, ha₂⟩ => by
    rcases exists_between ha₂ with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, ha₁.trans hb₁.le, hb₂⟩, hb₁⟩⟩

No Maximal Element in Left-Closed Right-Open Intervals

Informal description

For any two elements $x$ and $y$ in a preorder $\alpha$, the left-closed right-open interval $\text{Ico}(x, y)$ has no maximal element.

instNoMaxOrderElemIio instance

: NoMaxOrder (Set.Iio x)

Full source

instance : NoMaxOrder (Set.Iio x) :=
  ⟨fun ⟨a, ha⟩ => by
    rcases exists_between ha with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, hb₂⟩, hb₁⟩⟩

No Maximal Element in Left-Infinite Open Interval

Informal description

For any element $x$ in a preorder, the open interval $(-\infty, x)$ has no maximal element.

Set.Iic_False theorem

: Iic False = { False }

Full source

@[simp] lemma Iic_False : Iic False = {False} := by aesop

Interval characterization: $(-\infty, \text{False}] = \{\text{False}\}$ in the propositional order

Informal description

In the preorder of propositions, the left-infinite right-closed interval $(-\infty, \text{False}]$ is equal to the singleton set $\{\text{False}\}$.

Set.Iic_True theorem

: Iic True = univ

Full source

@[simp] lemma Iic_True : Iic True = univ := by aesop

Interval of Elements Below True Equals Universe

Informal description

In a preorder, the left-infinite right-closed interval containing all elements less than or equal to `True` is equal to the entire universe (i.e., the set of all elements). In other words, $\{x \mid x \leq \text{True}\} = \text{univ}$.

Set.Ici_False theorem

: Ici False = univ

Full source

@[simp] lemma Ici_False : Ici False = univ := by aesop

Universal Set as Interval from False

Informal description

The left-closed right-infinite interval $[\text{False}, \infty)$ in the preorder on `Prop` is equal to the universal set (containing all propositions).

Set.Ici_True theorem

: Ici True = { True }

Full source

@[simp] lemma Ici_True : Ici True = {True} := by aesop

Interval of True Equals Singleton True

Informal description

The left-closed right-infinite interval starting at the proposition `True` is equal to the singleton set containing `True`, i.e., $[\text{True}, \infty) = \{\text{True}\}$.

Set.Iio_False theorem

: Iio False = ∅

Full source

lemma Iio_False : Iio False = ∅ := by aesop

Empty Interval Below False in Boolean Preorder

Informal description

In the preorder of Boolean values, the left-infinite right-open interval $(-\infty, \text{False})$ is equal to the empty set, i.e., $\{x \mid x < \text{False}\} = \emptyset$.

Set.Iio_True theorem

: Iio True = { False }

Full source

@[simp] lemma Iio_True : Iio True = {False} := by aesop (add simp [Ioi, lt_iff_le_not_le])

Interval of Booleans Below True is False Singleton

Informal description

In the preorder of Boolean values, the left-infinite right-open interval $(-\infty, \text{True})$ is equal to the singleton set $\{\text{False}\}$.

Set.Ioi_False theorem

: Ioi False = { True }

Full source

@[simp] lemma Ioi_False : Ioi False = {True} := by aesop (add simp [Ioi, lt_iff_le_not_le])

Interval of `False` in Boolean Preorder: $(\text{False}, \infty) = \{\text{True}\}$

Informal description

In the preorder of Boolean values, the left-open right-infinite interval starting at `False` is equal to the singleton set containing `True`, i.e., $(\text{False}, \infty) = \{\text{True}\}$.

Set.Ioi_True theorem

: Ioi True = ∅

Full source

lemma Ioi_True : Ioi True = ∅ := by aesop

Empty Interval Above True in Boolean Preorder

Informal description

In the preorder of Boolean values, the left-open right-infinite interval starting at `True` is empty, i.e., $(\text{True}, \infty) = \emptyset$.