Mathlib.Order.Interval.Set.LinearOrder

Set.not_mem_Ici theorem

: c ∉ Ici a ↔ c < a

Full source

theorem not_mem_Ici : c ∉ Ici ac ∉ Ici a ↔ c < a :=
  not_le

Non-membership in Closed Right-Infinite Interval: $c \notin [a, \infty) \leftrightarrow c < a$

Informal description

For any elements $a$ and $c$ in a linear order, $c$ does not belong to the closed interval $[a, \infty)$ if and only if $c < a$.

Set.not_mem_Iic theorem

: c ∉ Iic b ↔ b < c

Full source

theorem not_mem_Iic : c ∉ Iic bc ∉ Iic b ↔ b < c :=
  not_le

Non-membership in Closed Lower Interval: $c \notin (-\infty, b] \leftrightarrow b < c$

Informal description

For any elements $b$ and $c$ in a linear order, $c$ does not belong to the closed interval $(-\infty, b]$ if and only if $b < c$.

Set.not_mem_Ioi theorem

: c ∉ Ioi a ↔ c ≤ a

Full source

theorem not_mem_Ioi : c ∉ Ioi ac ∉ Ioi a ↔ c ≤ a :=
  not_lt

Non-membership in Right-Open Infinite Interval Characterized by Inequality

Informal description

For any elements $a$ and $c$ in a linear order, $c$ does not belong to the open right-infinite interval $(a, \infty)$ if and only if $c$ is less than or equal to $a$, i.e., $c \notin (a, \infty) \leftrightarrow c \leq a$.

Set.not_mem_Iio theorem

: c ∉ Iio b ↔ b ≤ c

Full source

theorem not_mem_Iio : c ∉ Iio bc ∉ Iio b ↔ b ≤ c :=
  not_lt

Non-membership in Left-Infinite Open Interval

Informal description

For any elements $b$ and $c$ in a linear order, $c$ does not belong to the open interval $(-\infty, b)$ if and only if $b \leq c$.

Set.compl_Iic theorem

: (Iic a)ᶜ = Ioi a

Full source

@[simp]
theorem compl_Iic : (Iic a)ᶜ = Ioi a :=
  ext fun _ => not_le

Complement of Closed Lower Interval Equals Open Upper Interval

Informal description

For any element $a$ in a linearly ordered set, the complement of the closed interval $(-\infty, a]$ is the open interval $(a, \infty)$. In other words, $(Iic a)^c = Ioi a$.

Set.compl_Ici theorem

: (Ici a)ᶜ = Iio a

Full source

@[simp]
theorem compl_Ici : (Ici a)ᶜ = Iio a :=
  ext fun _ => not_le

Complement of Closed Right-Infinite Interval Equals Open Left-Infinite Interval

Informal description

The complement of the closed interval $[a, \infty)$ is the open interval $(-\infty, a)$, i.e., $[a, \infty)^c = (-\infty, a)$.

Set.compl_Iio theorem

: (Iio a)ᶜ = Ici a

Full source

@[simp]
theorem compl_Iio : (Iio a)ᶜ = Ici a :=
  ext fun _ => not_lt

Complement of $(-\infty, a)$ is $[a, \infty)$

Informal description

The complement of the left-infinite open interval $(-\infty, a)$ is the right-infinite closed interval $[a, \infty)$. In other words, $(Iio\, a)^c = Ici\, a$.

Set.compl_Ioi theorem

: (Ioi a)ᶜ = Iic a

Full source

@[simp]
theorem compl_Ioi : (Ioi a)ᶜ = Iic a :=
  ext fun _ => not_lt

Complement of Open Right Interval Equals Closed Left Interval

Informal description

For any element $a$ in a linear order, the complement of the open interval $(a, \infty)$ is the closed interval $(-\infty, a]$, i.e., $(a, \infty)^c = (-\infty, a]$.

Set.Ici_diff_Ici theorem

: Ici a \ Ici b = Ico a b

Full source

@[simp]
theorem Ici_diff_Ici : IciIci a \ Ici b = Ico a b := by rw [diff_eq, compl_Ici, Ici_inter_Iio]

Difference of Two Closed Right-Infinite Intervals Equals Left-Closed Right-Open Interval

Informal description

For any elements $a$ and $b$ in a linear order, the set difference between the closed right-infinite interval $[a, \infty)$ and the closed right-infinite interval $[b, \infty)$ is equal to the left-closed right-open interval $[a, b)$, i.e., $[a, \infty) \setminus [b, \infty) = [a, b)$.

Set.Ici_diff_Ioi theorem

: Ici a \ Ioi b = Icc a b

Full source

@[simp]
theorem Ici_diff_Ioi : IciIci a \ Ioi b = Icc a b := by rw [diff_eq, compl_Ioi, Ici_inter_Iic]

Difference of Closed-Left and Open-Right Intervals Equals Closed Interval $[a, b]$

Informal description

For any elements $a$ and $b$ in a linear order, the difference between the closed interval $[a, \infty)$ and the open interval $(b, \infty)$ is the closed-closed interval $[a, b]$, i.e., $[a, \infty) \setminus (b, \infty) = [a, b]$.

Set.Ioi_diff_Ioi theorem

: Ioi a \ Ioi b = Ioc a b

Full source

@[simp]
theorem Ioi_diff_Ioi : IoiIoi a \ Ioi b = Ioc a b := by rw [diff_eq, compl_Ioi, Ioi_inter_Iic]

Difference of Two Open Right Intervals Equals Half-Open Interval

Informal description

For any elements $a$ and $b$ in a linear order, the set difference between the open interval $(a, \infty)$ and the open interval $(b, \infty)$ is the half-open interval $(a, b]$, i.e., $(a, \infty) \setminus (b, \infty) = (a, b]$.

Set.Ioi_diff_Ici theorem

: Ioi a \ Ici b = Ioo a b

Full source

@[simp]
theorem Ioi_diff_Ici : IoiIoi a \ Ici b = Ioo a b := by rw [diff_eq, compl_Ici, Ioi_inter_Iio]

Difference of Open and Closed Right-Infinite Intervals is Open Interval

Informal description

The set difference between the open right-infinite interval $(a, \infty)$ and the closed right-infinite interval $[b, \infty)$ is the open interval $(a, b)$, i.e., $(a, \infty) \setminus [b, \infty) = (a, b)$.

Set.Iic_diff_Iic theorem

: Iic b \ Iic a = Ioc a b

Full source

@[simp]
theorem Iic_diff_Iic : IicIic b \ Iic a = Ioc a b := by
  rw [diff_eq, compl_Iic, inter_comm, Ioi_inter_Iic]

Difference of Closed Lower Intervals Equals Half-Open Interval

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the set difference between the closed lower interval $(-\infty, b]$ and the closed lower interval $(-\infty, a]$ is equal to the half-open interval $(a, b]$. In other words, $(-\infty, b] \setminus (-\infty, a] = (a, b]$.

Set.Iio_diff_Iic theorem

: Iio b \ Iic a = Ioo a b

Full source

@[simp]
theorem Iio_diff_Iic : IioIio b \ Iic a = Ioo a b := by
  rw [diff_eq, compl_Iic, inter_comm, Ioi_inter_Iio]

Difference of Open Lower Interval and Closed Lower Interval Equals Open Interval $(a, b)$

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the set difference between the open interval $(-\infty, b)$ and the closed interval $(-\infty, a]$ is the open interval $(a, b)$. In other words, $Iio\, b \setminus Iic\, a = Ioo\, a\, b$.

Set.Iic_diff_Iio theorem

: Iic b \ Iio a = Icc a b

Full source

@[simp]
theorem Iic_diff_Iio : IicIic b \ Iio a = Icc a b := by
  rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iic]

Difference of Left-Infinite Intervals Equals Closed Interval

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the set difference between the closed left-infinite interval $(-\infty, b]$ and the open left-infinite interval $(-\infty, a)$ is equal to the closed interval $[a, b]$. In other words, $(-\infty, b] \setminus (-\infty, a) = [a, b]$.

Set.Iio_diff_Iio theorem

: Iio b \ Iio a = Ico a b

Full source

@[simp]
theorem Iio_diff_Iio : IioIio b \ Iio a = Ico a b := by
  rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iio]

Difference of Left-Infinite Open Intervals Equals Left-Closed Right-Open Interval

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the set difference between the left-infinite open interval $(-\infty, b)$ and the left-infinite open interval $(-\infty, a)$ is equal to the left-closed right-open interval $[a, b)$. In other words, $(-\infty, b) \setminus (-\infty, a) = [a, b)$.

Set.Ioi_injective theorem

: Injective (Ioi : α → Set α)

Full source

theorem Ioi_injective : Injective (Ioi : α → Set α) := fun _ _ =>
  eq_of_forall_gt_iffeq_of_forall_gt_iff ∘ Set.ext_iff.1

Injectivity of Right-Infinite Open Interval Construction

Informal description

For any linearly ordered type $\alpha$, the function $a \mapsto (a, \infty)$ (the open right-infinite interval) is injective. That is, if $(a, \infty) = (b, \infty)$, then $a = b$.

Set.Iio_injective theorem

: Injective (Iio : α → Set α)

Full source

theorem Iio_injective : Injective (Iio : α → Set α) := fun _ _ =>
  eq_of_forall_lt_iffeq_of_forall_lt_iff ∘ Set.ext_iff.1

Injectivity of Left-Infinite Open Interval Construction in Linear Orders

Informal description

The function that maps each element $a$ in a linear order $\alpha$ to the left-infinite open interval $(-\infty, a)$ is injective. That is, for any $a, b \in \alpha$, if $(-\infty, a) = (-\infty, b)$, then $a = b$.

Set.Ioi_inj theorem

: Ioi a = Ioi b ↔ a = b

Full source

theorem Ioi_inj : IoiIoi a = Ioi b ↔ a = b :=
  Ioi_injective.eq_iff

Equality of Right-Infinite Open Intervals in Linear Orders

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the right-infinite open intervals $(a, \infty)$ and $(b, \infty)$ are equal if and only if $a = b$.

Set.Iio_inj theorem

: Iio a = Iio b ↔ a = b

Full source

theorem Iio_inj : IioIio a = Iio b ↔ a = b :=
  Iio_injective.eq_iff

Equality of Left-Infinite Open Intervals in Linear Orders

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the left-infinite open intervals $(-\infty, a)$ and $(-\infty, b)$ are equal if and only if $a = b$.

Set.Ico_subset_Ico_iff theorem

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

Full source

theorem Ico_subset_Ico_iff (h₁ : a₁ < b₁) : IcoIco a₁ b₁ ⊆ Ico a₂ b₂Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
  ⟨fun h =>
    have : a₂ ≤ a₁ ∧ a₁ < b₂ := h ⟨le_rfl, h₁⟩
    ⟨this.1, le_of_not_lt fun h' => lt_irrefl b₂ (h ⟨this.2.le, h'⟩).2⟩,
    fun ⟨h₁, h₂⟩ => Ico_subset_Ico h₁ h₂⟩

Subset Condition for Half-Open Intervals in Linear Orders

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a linearly ordered set with $a₁ < b₁$, the interval $[a₁, b₁)$ is a subset of $[a₂, b₂)$ if and only if $a₂ \leq a₁$ and $b₁ \leq b₂$.

Set.Ioc_subset_Ioc_iff theorem

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

Full source

theorem Ioc_subset_Ioc_iff (h₁ : a₁ < b₁) : IocIoc a₁ b₁ ⊆ Ioc a₂ b₂Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁ := by
  convert @Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁ using 2 <;> exact (@Ico_toDual α _ _ _).symm

Subset Condition for Right-Half-Open Intervals in Linear Orders: $(a₁, b₁] \subseteq (a₂, b₂] \iff b₁ \leq b₂ \land a₂ \leq a₁$

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a linearly ordered set with $a₁ < b₁$, the interval $(a₁, b₂]$ is a subset of $(a₂, b₂]$ if and only if $b₁ \leq b₂$ and $a₂ \leq a₁$.

Set.Ioo_subset_Ioo_iff theorem

[DenselyOrdered α] (h₁ : a₁ < b₁) : Ioo a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Full source

theorem Ioo_subset_Ioo_iff [DenselyOrdered α] (h₁ : a₁ < b₁) :
    IooIoo a₁ b₁ ⊆ Ioo a₂ b₂Ioo a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
  ⟨fun h => by
    rcases exists_between h₁ with ⟨x, xa, xb⟩
    constructor <;> refine le_of_not_lt fun h' => ?_
    · have ab := (h ⟨xa, xb⟩).1.trans xb
      exact lt_irrefl _ (h ⟨h', ab⟩).1
    · have ab := xa.trans (h ⟨xa, xb⟩).2
      exact lt_irrefl _ (h ⟨ab, h'⟩).2,
    fun ⟨h₁, h₂⟩ => Ioo_subset_Ioo h₁ h₂⟩

Subset condition for open intervals in densely ordered sets: $(a₁, b₁) \subseteq (a₂, b₂) \iff a₂ \leq a₁ \land b₁ \leq b₂$

Informal description

Let $\alpha$ be a densely ordered set, and let $a₁, b₁, a₂, b₂ \in \alpha$ with $a₁ < b₁$. Then the open interval $(a₁, b₁)$ is a subset of the open interval $(a₂, b₂)$ if and only if $a₂ \leq a₁$ and $b₁ \leq b₂$.

Set.Ico_eq_Ico_iff theorem

(h : a₁ < b₁ ∨ a₂ < b₂) : Ico a₁ b₁ = Ico a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

Full source

theorem Ico_eq_Ico_iff (h : a₁ < b₁ ∨ a₂ < b₂) : IcoIco a₁ b₁ = Ico a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ :=
  ⟨fun e => by
      simp only [Subset.antisymm_iff] at e
      simp only [le_antisymm_iff]
      rcases h with h | h <;>
      simp only [gt_iff_lt, not_lt, Ico_subset_Ico_iff h] at e <;>
      [ rcases e with ⟨⟨h₁, h₂⟩, e'⟩; rcases e with ⟨e', ⟨h₁, h₂⟩⟩ ] <;>
      have hab := (Ico_subset_Ico_iff <| h₁.trans_lt <| h.trans_le h₂).1 e' <;>
      tauto,
    fun ⟨h₁, h₂⟩ => by rw [h₁, h₂]⟩

Equality Condition for Half-Open Intervals in Linear Orders: $[a₁, b₁) = [a₂, b₂) \iff a₁ = a₂ \land b₁ = b₂$

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a linearly ordered set, if either $a₁ < b₁$ or $a₂ < b₂$, then the half-open intervals $[a₁, b₁)$ and $[a₂, b₂)$ are equal if and only if $a₁ = a₂$ and $b₁ = b₂$.

Set.Ici_eq_singleton_iff_isTop theorem

{x : α} : (Ici x = { x }) ↔ IsTop x

Full source

lemma Ici_eq_singleton_iff_isTop {x : α} : (Ici x = {x}) ↔ IsTop x := by
  refine ⟨fun h y ↦ ?_, fun h ↦ by ext y; simp [(h y).ge_iff_eq]⟩
  by_contra! H
  have : y ∈ Ici x := H.le
  rw [h, mem_singleton_iff] at this
  exact lt_irrefl y (this.le.trans_lt H)

Singleton Closed-Infinite Interval Equals Top Element

Informal description

For any element $x$ in a linearly ordered type $\alpha$, the closed-infinite interval $[x, \infty)$ is equal to the singleton set $\{x\}$ if and only if $x$ is the top element of $\alpha$.

Set.Ioi_subset_Ioi_iff theorem

: Ioi b ⊆ Ioi a ↔ a ≤ b

Full source

@[simp]
theorem Ioi_subset_Ioi_iff : IoiIoi b ⊆ Ioi aIoi b ⊆ Ioi a ↔ a ≤ b := by
  refine ⟨fun h => ?_, Ioi_subset_Ioi⟩
  by_contra ba
  exact lt_irrefl _ (h (not_le.mp ba))

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

Informal description

For any elements $a, b$ in a linearly ordered type $\alpha$, the open interval $(b, \infty)$ is contained in the open interval $(a, \infty)$ if and only if $a \leq b$.

Set.Ioi_ssubset_Ioi_iff theorem

: Ioi b ⊂ Ioi a ↔ a < b

Full source

@[simp]
theorem Ioi_ssubset_Ioi_iff : IoiIoi b ⊂ Ioi aIoi b ⊂ Ioi a ↔ a < b := by
  refine ⟨fun h => ?_, Ioi_ssubset_Ioi⟩
  obtain ⟨_, c, ac, cb⟩ := ssubset_iff_exists.mp h
  exact ac.trans_le (le_of_not_lt cb)

Strict Subset Relation Between Right-Infinite Open Intervals: $(b, \infty) \subset (a, \infty) \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the open right-infinite interval $(b, \infty)$ is a strict subset of $(a, \infty)$ if and only if $a < b$.

Set.Ioi_subset_Ici_iff theorem

[DenselyOrdered α] : Ioi b ⊆ Ici a ↔ a ≤ b

Full source

@[simp]
theorem Ioi_subset_Ici_iff [DenselyOrdered α] : IoiIoi b ⊆ Ici aIoi b ⊆ Ici a ↔ a ≤ b := by
  refine ⟨fun h => ?_, Ioi_subset_Ici⟩
  by_contra ba
  obtain ⟨c, bc, ca⟩ : ∃ c, b < c ∧ c < a := exists_between (not_le.mp ba)
  exact lt_irrefl _ (ca.trans_le (h bc))

Inclusion of Right-Infinite Intervals in Densely Ordered Sets: $(b, \infty) \subseteq [a, \infty) \leftrightarrow a \leq b$

Informal description

Let $\alpha$ be a densely ordered type. For any elements $a, b \in \alpha$, the open interval $(b, \infty)$ is contained in the closed interval $[a, \infty)$ if and only if $a \leq b$.

Set.Iio_subset_Iio_iff theorem

: Iio a ⊆ Iio b ↔ a ≤ b

Full source

@[simp]
theorem Iio_subset_Iio_iff : IioIio a ⊆ Iio bIio a ⊆ Iio b ↔ a ≤ b := by
  refine ⟨fun h => ?_, Iio_subset_Iio⟩
  by_contra ab
  exact lt_irrefl _ (h (not_le.mp ab))

Subset Relation Between Left-Infinite Open Intervals in Linear Orders

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the left-infinite open interval $(-\infty, a)$ is a subset of the left-infinite open interval $(-\infty, b)$ if and only if $a \leq b$.

Set.Iio_ssubset_Iio_iff theorem

: Iio a ⊂ Iio b ↔ a < b

Full source

@[simp]
theorem Iio_ssubset_Iio_iff : IioIio a ⊂ Iio bIio a ⊂ Iio b ↔ a < b := by
  refine ⟨fun h => ?_, Iio_ssubset_Iio⟩
  obtain ⟨_, c, cb, ac⟩ := ssubset_iff_exists.mp h
  exact (le_of_not_lt ac).trans_lt cb

Strict Subset Relation Between Left-Infinite Open Intervals: $(-\infty, a) \subset (-\infty, b) \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the left-infinite open interval $(-\infty, a)$ is a strict subset of the left-infinite open interval $(-\infty, b)$ if and only if $a < b$.

Set.Iio_subset_Iic_iff theorem

[DenselyOrdered α] : Iio a ⊆ Iic b ↔ a ≤ b

Full source

@[simp]
theorem Iio_subset_Iic_iff [DenselyOrdered α] : IioIio a ⊆ Iic bIio a ⊆ Iic b ↔ a ≤ b := by
  rw [← diff_eq_empty, Iio_diff_Iic, Ioo_eq_empty_iff, not_lt]

Subset Relation Between Open Lower and Closed Lower Intervals in Densely Ordered Sets

Informal description

In a densely ordered type $\alpha$, the left-infinite open interval $(-\infty, a)$ is a subset of the left-infinite closed interval $(-\infty, b]$ if and only if $a \leq b$.

Set.Iic_union_Ioi_of_le theorem

(h : a ≤ b) : Iic b ∪ Ioi a = univ

Full source

theorem Iic_union_Ioi_of_le (h : a ≤ b) : IicIic b ∪ Ioi a = univ :=
  eq_univ_of_forall fun x => (h.lt_or_le x).symm

Union of $(-\infty, b]$ and $(a, \infty)$ equals universe when $a \leq b$

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$ with $a \leq b$, the union of the closed interval $(-\infty, b]$ and the open interval $(a, \infty)$ is the entire space $\alpha$.

Set.Iio_union_Ici_of_le theorem

(h : a ≤ b) : Iio b ∪ Ici a = univ

Full source

theorem Iio_union_Ici_of_le (h : a ≤ b) : IioIio b ∪ Ici a = univ :=
  eq_univ_of_forall fun x => (h.le_or_lt x).symm

Union of Open Lower and Closed Upper Intervals Covers Entire Space When $a \leq b$

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$ such that $a \leq b$, the union of the open interval $(-\infty, b)$ and the closed interval $[a, \infty)$ is the entire space $\alpha$.

Set.Iic_union_Ici_of_le theorem

(h : a ≤ b) : Iic b ∪ Ici a = univ

Full source

theorem Iic_union_Ici_of_le (h : a ≤ b) : IicIic b ∪ Ici a = univ :=
  eq_univ_of_forall fun x => (h.le_or_le x).symm

Union of complementary closed intervals covers entire space under order condition

Informal description

For any elements $a$ and $b$ in a linear order with $a \leq b$, the union of the closed interval $(-\infty, b]$ and the closed interval $[a, \infty)$ is the entire space.

Set.Iio_union_Ioi_of_lt theorem

(h : a < b) : Iio b ∪ Ioi a = univ

Full source

theorem Iio_union_Ioi_of_lt (h : a < b) : IioIio b ∪ Ioi a = univ :=
  eq_univ_of_forall fun x => (h.lt_or_lt x).symm

Union of Open Intervals Covers Universe When $a < b$

Informal description

For any elements $a$ and $b$ in a linear order such that $a < b$, the union of the open left-infinite interval $(-\infty, b)$ and the open right-infinite interval $(a, \infty)$ is the entire universe of the type.

Set.Iic_union_Ici theorem

: Iic a ∪ Ici a = univ

Full source

@[simp]
theorem Iic_union_Ici : IicIic a ∪ Ici a = univ :=
  Iic_union_Ici_of_le le_rfl

Union of Closed Intervals Covering Entire Space at $a$

Informal description

For any element $a$ in a linear order, the union of the closed left-infinite interval $(-\infty, a]$ and the closed right-infinite interval $[a, \infty)$ is the entire space.

Set.Iio_union_Ici theorem

: Iio a ∪ Ici a = univ

Full source

@[simp]
theorem Iio_union_Ici : IioIio a ∪ Ici a = univ :=
  Iio_union_Ici_of_le le_rfl

Union of Open Lower and Closed Upper Intervals Covers Entire Space

Informal description

For any element $a$ in a linearly ordered type, the union of the open left-infinite interval $(-\infty, a)$ and the closed right-infinite interval $[a, \infty)$ is the entire space.

Set.Iic_union_Ioi theorem

: Iic a ∪ Ioi a = univ

Full source

@[simp]
theorem Iic_union_Ioi : IicIic a ∪ Ioi a = univ :=
  Iic_union_Ioi_of_le le_rfl

Union of $(-\infty, a]$ and $(a, \infty)$ equals universe

Informal description

For any element $a$ in a linearly ordered type, the union of the closed interval $(-\infty, a]$ and the open interval $(a, \infty)$ is the entire space.

Set.Iio_union_Ioi theorem

: Iio a ∪ Ioi a = { a }ᶜ

Full source

@[simp]
theorem Iio_union_Ioi : IioIio a ∪ Ioi a = {a}{a}ᶜ :=
  ext fun _ => lt_or_lt_iff_ne

Union of Open Intervals Around a Point Equals Its Complement

Informal description

For any element $a$ in a linear order, the union of the open interval $(-\infty, a)$ and the open interval $(a, \infty)$ is equal to the complement of the singleton set $\{a\}$, i.e., $(-\infty, a) \cup (a, \infty) = \{a\}^c$.

Set.Ioo_union_Ioi' theorem

(h₁ : c < b) : Ioo a b ∪ Ioi c = Ioi (min a c)

Full source

theorem Ioo_union_Ioi' (h₁ : c < b) : IooIoo a b ∪ Ioi c = Ioi (min a c) := by
  ext1 x
  simp_rw [mem_union, mem_Ioo, mem_Ioi, min_lt_iff]
  by_cases hc : c < x
  · tauto
  · have hxb : x < b := (le_of_not_gt hc).trans_lt h₁
    tauto

Union of open interval and open ray equals open ray: $(a, b) \cup (c, \infty) = (\min(a, c), \infty)$ when $c < b$

Informal description

For real numbers $a, b, c$ with $c < b$, the union of the open interval $(a, b)$ and the open ray $(c, \infty)$ equals the open ray $(\min(a, c), \infty)$.

Set.Ioo_union_Ioi theorem

(h : c < max a b) : Ioo a b ∪ Ioi c = Ioi (min a c)

Full source

theorem Ioo_union_Ioi (h : c < max a b) : IooIoo a b ∪ Ioi c = Ioi (min a c) := by
  rcases le_total a b with hab | hab <;> simp [hab] at h
  · exact Ioo_union_Ioi' h
  · rw [min_comm]
    simp [*, min_eq_left_of_lt]

Union of Open Interval and Open Ray Equals Open Ray: $(a, b) \cup (c, \infty) = (\min(a, c), \infty)$ when $c < \max(a, b)$

Informal description

For any elements $a, b, c$ in a linear order with $c < \max(a, b)$, the union of the open interval $(a, b)$ and the open ray $(c, \infty)$ equals the open ray $(\min(a, c), \infty)$.

Set.Ioi_subset_Ioo_union_Ici theorem

: Ioi a ⊆ Ioo a b ∪ Ici b

Full source

theorem Ioi_subset_Ioo_union_Ici : IoiIoi a ⊆ Ioo a b ∪ Ici b := fun x hx =>
  (lt_or_le x b).elim (fun hxb => Or.inl ⟨hx, hxb⟩) fun hxb => Or.inr hxb

Decomposition of Right-Infinite Interval into Open and Closed Parts

Informal description

For any real numbers $a$ and $b$, the open right-infinite interval $(a, \infty)$ is contained in the union of the open interval $(a, b)$ and the closed right-infinite interval $[b, \infty)$.

Set.Ioo_union_Ici_eq_Ioi theorem

(h : a < b) : Ioo a b ∪ Ici b = Ioi a

Full source

@[simp]
theorem Ioo_union_Ici_eq_Ioi (h : a < b) : IooIoo a b ∪ Ici b = Ioi a :=
  Subset.antisymm (fun _ hx => hx.elim And.left h.trans_le) Ioi_subset_Ioo_union_Ici

Union of Open and Closed Right-Infinite Intervals Equals Right-Infinite Interval

Informal description

For any elements $a$ and $b$ in a linear order with $a < b$, the union of the open interval $(a, b)$ and the closed right-infinite interval $[b, \infty)$ equals the open right-infinite interval $(a, \infty)$. That is, $(a, b) \cup [b, \infty) = (a, \infty)$.

Set.Ici_subset_Ico_union_Ici theorem

: Ici a ⊆ Ico a b ∪ Ici b

Full source

theorem Ici_subset_Ico_union_Ici : IciIci a ⊆ Ico a b ∪ Ici b := fun x hx =>
  (lt_or_le x b).elim (fun hxb => Or.inl ⟨hx, hxb⟩) fun hxb => Or.inr hxb

Inclusion of Closed Interval in Union of Half-Open and Closed Intervals

Informal description

For any elements $a$ and $b$ in a linear order, the closed interval $[a, \infty)$ is contained in the union of the half-open interval $[a, b)$ and the closed interval $[b, \infty)$. In other words, $[a, \infty) \subseteq [a, b) \cup [b, \infty)$.

Set.Ico_union_Ici_eq_Ici theorem

(h : a ≤ b) : Ico a b ∪ Ici b = Ici a

Full source

@[simp]
theorem Ico_union_Ici_eq_Ici (h : a ≤ b) : IcoIco a b ∪ Ici b = Ici a :=
  Subset.antisymm (fun _ hx => hx.elim And.left h.trans) Ici_subset_Ico_union_Ici

Union of Half-Open and Closed Intervals Equals Closed Interval: $[a, b) \cup [b, \infty) = [a, \infty)$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a linear order with $a \leq b$, the union of the half-open interval $[a, b)$ and the closed interval $[b, \infty)$ is equal to the closed interval $[a, \infty)$. That is, $[a, b) \cup [b, \infty) = [a, \infty)$.

Set.Ico_union_Ici' theorem

(h₁ : c ≤ b) : Ico a b ∪ Ici c = Ici (min a c)

Full source

theorem Ico_union_Ici' (h₁ : c ≤ b) : IcoIco a b ∪ Ici c = Ici (min a c) := by
  ext1 x
  simp_rw [mem_union, mem_Ico, mem_Ici, min_le_iff]
  by_cases hc : c ≤ x
  · tauto
  · have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
    tauto

Union of Half-Open and Closed Intervals in Linear Order: $[a, b) \cup [c, \infty) = [\min(a, c), \infty)$ when $c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a linear order, if $c \leq b$, then the union of the half-open interval $[a, b)$ and the closed interval $[c, \infty)$ is equal to the closed interval $[\min(a, c), \infty)$.

Set.Ico_union_Ici theorem

(h : c ≤ max a b) : Ico a b ∪ Ici c = Ici (min a c)

Full source

theorem Ico_union_Ici (h : c ≤ max a b) : IcoIco a b ∪ Ici c = Ici (min a c) := by
  rcases le_total a b with hab | hab <;> simp [hab] at h
  · exact Ico_union_Ici' h
  · simp [*]

Union of Half-Open and Closed Intervals: $[a, b) \cup [c, \infty) = [\min(a, c), \infty)$ when $c \leq \max(a, b)$

Informal description

For any elements $a$, $b$, and $c$ in a linear order, if $c \leq \max(a, b)$, then the union of the half-open interval $[a, b)$ and the closed interval $[c, \infty)$ is equal to the closed interval $[\min(a, c), \infty)$. That is, $[a, b) \cup [c, \infty) = [\min(a, c), \infty)$.

Set.Ioi_subset_Ioc_union_Ioi theorem

: Ioi a ⊆ Ioc a b ∪ Ioi b

Full source

theorem Ioi_subset_Ioc_union_Ioi : IoiIoi a ⊆ Ioc a b ∪ Ioi b := fun x hx =>
  (le_or_lt x b).elim (fun hxb => Or.inl ⟨hx, hxb⟩) fun hxb => Or.inr hxb

Open Interval Decomposition: $(a, \infty) \subseteq (a, b] \cup (b, \infty)$

Informal description

For any elements $a$ and $b$ in a linear order, the open interval $(a, \infty)$ is a subset of the union of the half-open interval $(a, b]$ and the open interval $(b, \infty)$. In other words, $(a, \infty) \subseteq (a, b] \cup (b, \infty)$.

Set.Ioc_union_Ioi_eq_Ioi theorem

(h : a ≤ b) : Ioc a b ∪ Ioi b = Ioi a

Full source

@[simp]
theorem Ioc_union_Ioi_eq_Ioi (h : a ≤ b) : IocIoc a b ∪ Ioi b = Ioi a :=
  Subset.antisymm (fun _ hx => hx.elim And.left h.trans_lt) Ioi_subset_Ioc_union_Ioi

Union of Half-Open and Open Intervals Equals Open Ray: $(a, b] \cup (b, \infty) = (a, \infty)$

Informal description

For any elements $a$ and $b$ in a linear order with $a \leq b$, the union of the half-open interval $(a, b]$ and the open interval $(b, \infty)$ equals the open interval $(a, \infty)$. In other words, $(a, b] \cup (b, \infty) = (a, \infty)$.

Set.Ioc_union_Ioi' theorem

(h₁ : c ≤ b) : Ioc a b ∪ Ioi c = Ioi (min a c)

Full source

theorem Ioc_union_Ioi' (h₁ : c ≤ b) : IocIoc a b ∪ Ioi c = Ioi (min a c) := by
  ext1 x
  simp_rw [mem_union, mem_Ioc, mem_Ioi, min_lt_iff]
  by_cases hc : c < x
  · tauto
  · have hxb : x ≤ b := (le_of_not_gt hc).trans h₁
    tauto

Union of Half-Open Interval and Open Ray Equals Open Ray from Minimum

Informal description

For any elements $a$, $b$, and $c$ in a linear order, if $c \leq b$, then the union of the half-open interval $(a, b]$ and the open ray $(c, \infty)$ equals the open ray $(\min(a, c), \infty)$.

Set.Ioc_union_Ioi theorem

(h : c ≤ max a b) : Ioc a b ∪ Ioi c = Ioi (min a c)

Full source

theorem Ioc_union_Ioi (h : c ≤ max a b) : IocIoc a b ∪ Ioi c = Ioi (min a c) := by
  rcases le_total a b with hab | hab <;> simp [hab] at h
  · exact Ioc_union_Ioi' h
  · simp [*]

Union of Half-Open Interval and Open Ray Equals Open Ray from Minimum under Max Condition

Informal description

For any elements $a$, $b$, and $c$ in a linear order, if $c \leq \max(a, b)$, then the union of the half-open interval $(a, b]$ and the open ray $(c, \infty)$ equals the open ray $(\min(a, c), \infty)$.

Set.Ici_subset_Icc_union_Ioi theorem

: Ici a ⊆ Icc a b ∪ Ioi b

Full source

theorem Ici_subset_Icc_union_Ioi : IciIci a ⊆ Icc a b ∪ Ioi b := fun x hx =>
  (le_or_lt x b).elim (fun hxb => Or.inl ⟨hx, hxb⟩) fun hxb => Or.inr hxb

Inclusion of Closed-Infinite Interval in Union of Closed and Open-Infinite Intervals

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the closed-infinite interval $[a, \infty)$ is a subset of the union of the closed interval $[a, b]$ and the open-infinite interval $(b, \infty)$. In other words, $[a, \infty) \subseteq [a, b] \cup (b, \infty)$.

Set.Icc_union_Ioi_eq_Ici theorem

(h : a ≤ b) : Icc a b ∪ Ioi b = Ici a

Full source

@[simp]
theorem Icc_union_Ioi_eq_Ici (h : a ≤ b) : IccIcc a b ∪ Ioi b = Ici a :=
  Subset.antisymm (fun _ hx => (hx.elim And.left) fun hx' => h.trans <| le_of_lt hx')
    Ici_subset_Icc_union_Ioi

Union of Closed and Open-Infinite Intervals Equals Closed-Infinite Interval

Informal description

For any elements $a$ and $b$ in a linearly ordered set with $a \leq b$, the union of the closed interval $[a, b]$ and the open-infinite interval $(b, \infty)$ equals the closed-infinite interval $[a, \infty)$. In other words, $[a, b] \cup (b, \infty) = [a, \infty)$.

Set.Ioi_subset_Ioc_union_Ici theorem

: Ioi a ⊆ Ioc a b ∪ Ici b

Full source

theorem Ioi_subset_Ioc_union_Ici : IoiIoi a ⊆ Ioc a b ∪ Ici b :=
  Subset.trans Ioi_subset_Ioo_union_Ici (union_subset_union_left _ Ioo_subset_Ioc_self)

Decomposition of $(a, \infty)$ into $(a, b]$ and $[b, \infty)$

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the open right-infinite interval $(a, \infty)$ is contained in the union of the half-open interval $(a, b]$ and the closed right-infinite interval $[b, \infty)$. That is, $(a, \infty) \subseteq (a, b] \cup [b, \infty)$.

Set.Ioc_union_Ici_eq_Ioi theorem

(h : a < b) : Ioc a b ∪ Ici b = Ioi a

Full source

@[simp]
theorem Ioc_union_Ici_eq_Ioi (h : a < b) : IocIoc a b ∪ Ici b = Ioi a :=
  Subset.antisymm (fun _ hx => hx.elim And.left h.trans_le) Ioi_subset_Ioc_union_Ici

Union of Half-Open and Closed-Infinite Intervals Equals Open-Infinite Interval: $(a, b] \cup [b, \infty) = (a, \infty)$

Informal description

For any elements $a$ and $b$ in a linearly ordered set with $a < b$, the union of the half-open interval $(a, b]$ and the closed-infinite interval $[b, \infty)$ equals the open-infinite interval $(a, \infty)$. That is, $(a, b] \cup [b, \infty) = (a, \infty)$.

Set.Ici_subset_Icc_union_Ici theorem

: Ici a ⊆ Icc a b ∪ Ici b

Full source

theorem Ici_subset_Icc_union_Ici : IciIci a ⊆ Icc a b ∪ Ici b :=
  Subset.trans Ici_subset_Ico_union_Ici (union_subset_union_left _ Ico_subset_Icc_self)

Inclusion of $[a, \infty)$ in $[a, b] \cup [b, \infty)$

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the closed-infinite interval $[a, \infty)$ is contained in the union of the closed interval $[a, b]$ and the closed-infinite interval $[b, \infty)$. In other words, $[a, \infty) \subseteq [a, b] \cup [b, \infty)$.

Set.Icc_union_Ici_eq_Ici theorem

(h : a ≤ b) : Icc a b ∪ Ici b = Ici a

Full source

@[simp]
theorem Icc_union_Ici_eq_Ici (h : a ≤ b) : IccIcc a b ∪ Ici b = Ici a :=
  Subset.antisymm (fun _ hx => hx.elim And.left h.trans) Ici_subset_Icc_union_Ici

Union of Closed Interval and Closed-Infinite Interval Equals Closed-Infinite Interval: $[a, b] \cup [b, \infty) = [a, \infty)$

Informal description

For any elements $a$ and $b$ in a linearly ordered set, if $a \leq b$, then the union of the closed interval $[a, b]$ and the closed-infinite interval $[b, \infty)$ is equal to the closed-infinite interval $[a, \infty)$. In other words, $[a, b] \cup [b, \infty) = [a, \infty)$.

Set.Icc_union_Ici' theorem

(h₁ : c ≤ b) : Icc a b ∪ Ici c = Ici (min a c)

Full source

theorem Icc_union_Ici' (h₁ : c ≤ b) : IccIcc a b ∪ Ici c = Ici (min a c) := by
  ext1 x
  simp_rw [mem_union, mem_Icc, mem_Ici, min_le_iff]
  by_cases hc : c ≤ x
  · tauto
  · have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
    tauto

Union of Closed Interval and Closed-Infinite Interval Equals Larger Closed-Infinite Interval

Informal description

For any elements $a$, $b$, and $c$ in a linear order, if $c \leq b$, then the union of the closed interval $[a, b]$ and the closed-infinite interval $[c, \infty)$ is equal to the closed-infinite interval $[\min(a, c), \infty)$.

Set.Icc_union_Ici theorem

(h : c ≤ max a b) : Icc a b ∪ Ici c = Ici (min a c)

Full source

theorem Icc_union_Ici (h : c ≤ max a b) : IccIcc a b ∪ Ici c = Ici (min a c) := by
  rcases le_or_lt a b with hab | hab <;> simp [hab] at h
  · exact Icc_union_Ici' h
  · rcases h with h | h
    · simp [*]
    · have hca : c ≤ a := h.trans hab.le
      simp [*]

Union of Closed Interval and Closed-Infinite Interval Equals Closed-Infinite Interval Starting at Minimum

Informal description

For any elements $a$, $b$, and $c$ in a linear order, if $c \leq \max(a, b)$, then the union of the closed interval $[a, b]$ and the closed-infinite interval $[c, \infty)$ is equal to the closed-infinite interval $[\min(a, c), \infty)$.

Set.Iic_subset_Iio_union_Icc theorem

: Iic b ⊆ Iio a ∪ Icc a b

Full source

theorem Iic_subset_Iio_union_Icc : IicIic b ⊆ Iio a ∪ Icc a b := fun x hx =>
  (lt_or_le x a).elim (fun hxa => Or.inl hxa) fun hxa => Or.inr ⟨hxa, hx⟩

Decomposition of Closed Lower Interval into Open Lower and Closed Subinterval

Informal description

For any elements $a$ and $b$ in a linear order, the closed interval $(-\infty, b]$ is contained in the union of the open interval $(-\infty, a)$ and the closed interval $[a, b]$. In other words, $(-\infty, b] \subseteq (-\infty, a) \cup [a, b]$.

Set.Iio_union_Icc_eq_Iic theorem

(h : a ≤ b) : Iio a ∪ Icc a b = Iic b

Full source

@[simp]
theorem Iio_union_Icc_eq_Iic (h : a ≤ b) : IioIio a ∪ Icc a b = Iic b :=
  Subset.antisymm (fun _ hx => hx.elim (fun hx => (le_of_lt hx).trans h) And.right)
    Iic_subset_Iio_union_Icc

Union of Open Lower and Closed Subinterval Equals Closed Lower Interval

Informal description

For any elements $a$ and $b$ in a linear order with $a \leq b$, the union of the open interval $(-\infty, a)$ and the closed interval $[a, b]$ equals the closed interval $(-\infty, b]$, i.e., $(-\infty, a) \cup [a, b] = (-\infty, b]$.

Set.Iio_subset_Iio_union_Ico theorem

: Iio b ⊆ Iio a ∪ Ico a b

Full source

theorem Iio_subset_Iio_union_Ico : IioIio b ⊆ Iio a ∪ Ico a b := fun x hx =>
  (lt_or_le x a).elim (fun hxa => Or.inl hxa) fun hxa => Or.inr ⟨hxa, hx⟩

Inclusion of Left-Infinite Open Interval in Union of Left-Infinite Open and Left-Closed Right-Open Intervals

Informal description

For any elements $a$ and $b$ in a linear order, the left-infinite open interval $(-\infty, b)$ is contained in the union of the left-infinite open interval $(-\infty, a)$ and the left-closed right-open interval $[a, b)$.

Set.Iio_union_Ico_eq_Iio theorem

(h : a ≤ b) : Iio a ∪ Ico a b = Iio b

Full source

@[simp]
theorem Iio_union_Ico_eq_Iio (h : a ≤ b) : IioIio a ∪ Ico a b = Iio b :=
  Subset.antisymm (fun _ hx => hx.elim (fun hx' => lt_of_lt_of_le hx' h) And.right)
    Iio_subset_Iio_union_Ico

Union of Open and Half-Open Intervals Equals Open Interval

Informal description

For any elements $a$ and $b$ in a linear order with $a \leq b$, the union of the left-infinite open interval $(-\infty, a)$ and the left-closed right-open interval $[a, b)$ equals the left-infinite open interval $(-\infty, b)$. In symbols: \[ (-\infty, a) \cup [a, b) = (-\infty, b) \]

Set.Iio_union_Ico' theorem

(h₁ : c ≤ b) : Iio b ∪ Ico c d = Iio (max b d)

Full source

theorem Iio_union_Ico' (h₁ : c ≤ b) : IioIio b ∪ Ico c d = Iio (max b d) := by
  ext1 x
  simp_rw [mem_union, mem_Iio, mem_Ico, lt_max_iff]
  by_cases hc : c ≤ x
  · tauto
  · have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
    tauto

Union of Open and Half-Open Intervals in Linear Order

Informal description

For any elements $a, b, c, d$ in a linear order, if $c \leq b$, then the union of the open interval $(-\infty, b)$ and the half-open interval $[c, d)$ equals the open interval $(-\infty, \max(b, d))$. In symbols: \[ (-\infty, b) \cup [c, d) = (-\infty, \max(b, d)) \]

Set.Iio_union_Ico theorem

(h : min c d ≤ b) : Iio b ∪ Ico c d = Iio (max b d)

Full source

theorem Iio_union_Ico (h : min c d ≤ b) : IioIio b ∪ Ico c d = Iio (max b d) := by
  rcases le_total c d with hcd | hcd <;> simp [hcd] at h
  · exact Iio_union_Ico' h
  · simp [*]

Union of Open and Half-Open Intervals Under Minimum Condition

Informal description

For any elements $b, c, d$ in a linear order, if $\min(c, d) \leq b$, then the union of the open interval $(-\infty, b)$ and the half-open interval $[c, d)$ equals the open interval $(-\infty, \max(b, d))$. In symbols: \[ (-\infty, b) \cup [c, d) = (-\infty, \max(b, d)) \]

Set.Iic_subset_Iic_union_Ioc theorem

: Iic b ⊆ Iic a ∪ Ioc a b

Full source

theorem Iic_subset_Iic_union_Ioc : IicIic b ⊆ Iic a ∪ Ioc a b := fun x hx =>
  (le_or_lt x a).elim (fun hxa => Or.inl hxa) fun hxa => Or.inr ⟨hxa, hx⟩

Inclusion of Closed Interval in Union of Closed and Half-Open Intervals

Informal description

For any elements $a$ and $b$ in a linear order, the closed interval $(-\infty, b]$ is a subset of the union of the closed interval $(-\infty, a]$ and the half-open interval $(a, b]$. In symbols: \[ (-\infty, b] \subseteq (-\infty, a] \cup (a, b] \]

Set.Iic_union_Ioc_eq_Iic theorem

(h : a ≤ b) : Iic a ∪ Ioc a b = Iic b

Full source

@[simp]
theorem Iic_union_Ioc_eq_Iic (h : a ≤ b) : IicIic a ∪ Ioc a b = Iic b :=
  Subset.antisymm (fun _ hx => hx.elim (fun hx' => le_trans hx' h) And.right)
    Iic_subset_Iic_union_Ioc

Union of Closed and Half-Open Intervals Equals Closed Interval

Informal description

For any elements $a$ and $b$ in a linear order with $a \leq b$, the union of the closed interval $(-\infty, a]$ and the half-open interval $(a, b]$ is equal to the closed interval $(-\infty, b]$. In symbols: \[ (-\infty, a] \cup (a, b] = (-\infty, b] \]

Set.Iic_union_Ioc' theorem

(h₁ : c < b) : Iic b ∪ Ioc c d = Iic (max b d)

Full source

theorem Iic_union_Ioc' (h₁ : c < b) : IicIic b ∪ Ioc c d = Iic (max b d) := by
  ext1 x
  simp_rw [mem_union, mem_Iic, mem_Ioc, le_max_iff]
  by_cases hc : c < x
  · tauto
  · have hxb : x ≤ b := (le_of_not_gt hc).trans h₁.le
    tauto

Union of Closed and Half-Open Intervals in Linear Order

Informal description

For any elements $a$, $b$, $c$, $d$ in a linear order, if $c < b$, then the union of the closed interval $(-\infty, b]$ and the half-open interval $(c, d]$ is equal to the closed interval $(-\infty, \max(b, d)]$. In symbols: \[ (-\infty, b] \cup (c, d] = (-\infty, \max(b, d)] \]

Set.Iic_union_Ioc theorem

(h : min c d < b) : Iic b ∪ Ioc c d = Iic (max b d)

Full source

theorem Iic_union_Ioc (h : min c d < b) : IicIic b ∪ Ioc c d = Iic (max b d) := by
  rcases le_total c d with hcd | hcd <;> simp [hcd] at h
  · exact Iic_union_Ioc' h
  · rw [max_comm]
    simp [*, max_eq_right_of_lt h]

Union of Closed and Half-Open Intervals in Linear Order with Minimum Condition

Informal description

For any elements $b$, $c$, $d$ in a linear order, if the minimum of $c$ and $d$ is less than $b$, then the union of the closed interval $(-\infty, b]$ and the half-open interval $(c, d]$ is equal to the closed interval $(-\infty, \max(b, d)]$. In symbols: \[ (-\infty, b] \cup (c, d] = (-\infty, \max(b, d)] \]

Set.Iio_subset_Iic_union_Ioo theorem

: Iio b ⊆ Iic a ∪ Ioo a b

Full source

theorem Iio_subset_Iic_union_Ioo : IioIio b ⊆ Iic a ∪ Ioo a b := fun x hx =>
  (le_or_lt x a).elim (fun hxa => Or.inl hxa) fun hxa => Or.inr ⟨hxa, hx⟩

Inclusion of $(-\infty, b)$ in $(-\infty, a] \cup (a, b)$ in linear orders

Informal description

For any elements $a$ and $b$ in a linear order, the interval $(-\infty, b)$ is contained in the union of $(-\infty, a]$ and $(a, b)$.

Set.Iic_union_Ioo_eq_Iio theorem

(h : a < b) : Iic a ∪ Ioo a b = Iio b

Full source

@[simp]
theorem Iic_union_Ioo_eq_Iio (h : a < b) : IicIic a ∪ Ioo a b = Iio b :=
  Subset.antisymm (fun _ hx => hx.elim (fun hx' => lt_of_le_of_lt hx' h) And.right)
    Iio_subset_Iic_union_Ioo

Union of $(-\infty, a]$ and $(a, b)$ equals $(-\infty, b)$ in linear orders

Informal description

For any elements $a$ and $b$ in a linear order with $a < b$, the union of the closed interval $(-\infty, a]$ and the open interval $(a, b)$ equals the open interval $(-\infty, b)$. In other words, $(-\infty, a] \cup (a, b) = (-\infty, b)$.

Set.Iio_union_Ioo' theorem

(h₁ : c < b) : Iio b ∪ Ioo c d = Iio (max b d)

Full source

theorem Iio_union_Ioo' (h₁ : c < b) : IioIio b ∪ Ioo c d = Iio (max b d) := by
  ext x
  rcases lt_or_le x b with hba | hba
  · simp [hba, h₁]
  · simp only [mem_Iio, mem_union, mem_Ioo, lt_max_iff]
    refine or_congr Iff.rfl ⟨And.right, ?_⟩
    exact fun h₂ => ⟨h₁.trans_le hba, h₂⟩

Union of $(-\infty, b)$ and $(c, d)$ is $(-\infty, \max(b, d))$ when $c < b$

Informal description

For real numbers $b, c, d$ with $c < b$, the union of the open interval $(-\infty, b)$ and the open interval $(c, d)$ equals the open interval $(-\infty, \max(b, d))$.

Set.Iio_union_Ioo theorem

(h : min c d < b) : Iio b ∪ Ioo c d = Iio (max b d)

Full source

theorem Iio_union_Ioo (h : min c d < b) : IioIio b ∪ Ioo c d = Iio (max b d) := by
  rcases le_total c d with hcd | hcd <;> simp [hcd] at h
  · exact Iio_union_Ioo' h
  · rw [max_comm]
    simp [*, max_eq_right_of_lt h]

Union of $(-\infty, b)$ and $(c, d)$ is $(-\infty, \max(b, d))$ under $\min(c, d) < b$

Informal description

For real numbers $b, c, d$ with $\min(c, d) < b$, the union of the open interval $(-\infty, b)$ and the open interval $(c, d)$ equals the open interval $(-\infty, \max(b, d))$.

Set.Iic_subset_Iic_union_Icc theorem

: Iic b ⊆ Iic a ∪ Icc a b

Full source

theorem Iic_subset_Iic_union_Icc : IicIic b ⊆ Iic a ∪ Icc a b :=
  Subset.trans Iic_subset_Iic_union_Ioc (union_subset_union_right _ Ioc_subset_Icc_self)

Inclusion of Closed-Infinite Interval in Union of Closed-Infinite and Closed Intervals

Informal description

For any elements $a$ and $b$ in a linear order, the closed interval $(-\infty, b]$ is a subset of the union of the closed interval $(-\infty, a]$ and the closed interval $[a, b]$. In symbols: \[ (-\infty, b] \subseteq (-\infty, a] \cup [a, b] \]

Set.Iic_union_Icc_eq_Iic theorem

(h : a ≤ b) : Iic a ∪ Icc a b = Iic b

Full source

@[simp]
theorem Iic_union_Icc_eq_Iic (h : a ≤ b) : IicIic a ∪ Icc a b = Iic b :=
  Subset.antisymm (fun _ hx => hx.elim (fun hx' => le_trans hx' h) And.right)
    Iic_subset_Iic_union_Icc

Union of $(-\infty, a]$ and $[a, b]$ equals $(-\infty, b]$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a linear order, if $a \leq b$, then the union of the closed-infinite interval $(-\infty, a]$ and the closed interval $[a, b]$ equals the closed-infinite interval $(-\infty, b]$. In symbols: $$(-\infty, a] \cup [a, b] = (-\infty, b] \quad \text{when } a \leq b.$$

Set.Iic_union_Icc' theorem

(h₁ : c ≤ b) : Iic b ∪ Icc c d = Iic (max b d)

Full source

theorem Iic_union_Icc' (h₁ : c ≤ b) : IicIic b ∪ Icc c d = Iic (max b d) := by
  ext1 x
  simp_rw [mem_union, mem_Iic, mem_Icc, le_max_iff]
  by_cases hc : c ≤ x
  · tauto
  · have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
    tauto

Union of Closed-Infinite and Closed Intervals under Condition $c \leq b$

Informal description

For any elements $a, b, c, d$ in a linear order, if $c \leq b$, then the union of the closed-infinite interval $(-\infty, b]$ and the closed interval $[c, d]$ equals the closed-infinite interval $(-\infty, \max(b, d)]$. In symbols: $$\text{Iic } b \cup \text{Icc } c d = \text{Iic } (\max(b, d)) \quad \text{when } c \leq b.$$

Set.Iic_union_Icc theorem

(h : min c d ≤ b) : Iic b ∪ Icc c d = Iic (max b d)

Full source

theorem Iic_union_Icc (h : min c d ≤ b) : IicIic b ∪ Icc c d = Iic (max b d) := by
  rcases le_or_lt c d with hcd | hcd <;> simp [hcd] at h
  · exact Iic_union_Icc' h
  · rcases h with h | h
    · have hdb : d ≤ b := hcd.le.trans h
      simp [*]
    · simp [*]

Union of Closed-Infinite and Closed Intervals under Minimum Condition

Informal description

For any elements $b, c, d$ in a linear order, if $\min(c, d) \leq b$, then the union of the closed-infinite interval $(-\infty, b]$ and the closed interval $[c, d]$ equals the closed-infinite interval $(-\infty, \max(b, d)]$. In symbols: $$(-\infty, b] \cup [c, d] = (-\infty, \max(b, d)] \quad \text{when } \min(c, d) \leq b.$$

Set.Iio_subset_Iic_union_Ico theorem

: Iio b ⊆ Iic a ∪ Ico a b

Full source

theorem Iio_subset_Iic_union_Ico : IioIio b ⊆ Iic a ∪ Ico a b :=
  Subset.trans Iio_subset_Iic_union_Ioo (union_subset_union_right _ Ioo_subset_Ico_self)

Inclusion of $(-\infty, b)$ in $(-\infty, a] \cup [a, b)$ in linear orders

Informal description

For any elements $a$ and $b$ in a linear order, the interval $(-\infty, b)$ is contained in the union of $(-\infty, a]$ and $[a, b)$. In symbols: $$(-\infty, b) \subseteq (-\infty, a] \cup [a, b).$$

Set.Iic_union_Ico_eq_Iio theorem

(h : a < b) : Iic a ∪ Ico a b = Iio b

Full source

@[simp]
theorem Iic_union_Ico_eq_Iio (h : a < b) : IicIic a ∪ Ico a b = Iio b :=
  Subset.antisymm (fun _ hx => hx.elim (fun hx' => lt_of_le_of_lt hx' h) And.right)
    Iio_subset_Iic_union_Ico

Union of Closed-Infinite and Half-Open Intervals Equals Open-Infinite Interval under Strict Inequality

Informal description

For any elements $a$ and $b$ in a linear order such that $a < b$, the union of the closed-infinite interval $(-\infty, a]$ and the left-closed right-open interval $[a, b)$ equals the open-infinite interval $(-\infty, b)$. In symbols: $$(-\infty, a] \cup [a, b) = (-\infty, b) \quad \text{when } a < b.$$

Set.Ioo_subset_Ioo_union_Ico theorem

: Ioo a c ⊆ Ioo a b ∪ Ico b c

Full source

theorem Ioo_subset_Ioo_union_Ico : IooIoo a c ⊆ Ioo a b ∪ Ico b c := fun x hx =>
  (lt_or_le x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Decomposition of Open Interval into Open and Left-Closed Right-Open Intervals

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the open interval $(a, c)$ is contained in the union of the open interval $(a, b)$ and the left-closed right-open interval $[b, c)$. That is, $(a, c) \subseteq (a, b) \cup [b, c)$.

Set.Ioo_union_Ico_eq_Ioo theorem

(h₁ : a < b) (h₂ : b ≤ c) : Ioo a b ∪ Ico b c = Ioo a c

Full source

@[simp]
theorem Ioo_union_Ico_eq_Ioo (h₁ : a < b) (h₂ : b ≤ c) : IooIoo a b ∪ Ico b c = Ioo a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans_le h₂⟩) fun hx => ⟨h₁.trans_le hx.1, hx.2⟩)
    Ioo_subset_Ioo_union_Ico

Union of Open and Half-Open Intervals Equals Open Interval: $(a, b) \cup [b, c) = (a, c)$ under $a < b \leq c$

Informal description

For any elements $a$, $b$, and $c$ in a linear order such that $a < b$ and $b \leq c$, the union of the open interval $(a, b)$ and the left-closed right-open interval $[b, c)$ equals the open interval $(a, c)$. That is, $(a, b) \cup [b, c) = (a, c)$.

Set.Ico_subset_Ico_union_Ico theorem

: Ico a c ⊆ Ico a b ∪ Ico b c

Full source

theorem Ico_subset_Ico_union_Ico : IcoIco a c ⊆ Ico a b ∪ Ico b c := fun x hx =>
  (lt_or_le x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Subset Property of Half-Open Intervals: $[a, c) \subseteq [a, b) \cup [b, c)$

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the interval $[a, c)$ is a subset of the union of the intervals $[a, b)$ and $[b, c)$.

Set.Ico_union_Ico_eq_Ico theorem

(h₁ : a ≤ b) (h₂ : b ≤ c) : Ico a b ∪ Ico b c = Ico a c

Full source

@[simp]
theorem Ico_union_Ico_eq_Ico (h₁ : a ≤ b) (h₂ : b ≤ c) : IcoIco a b ∪ Ico b c = Ico a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans_le h₂⟩) fun hx => ⟨h₁.trans hx.1, hx.2⟩)
    Ico_subset_Ico_union_Ico

Union of Adjacent Half-Open Intervals: $[a, b) \cup [b, c) = [a, c)$ when $a \leq b \leq c$

Informal description

For any elements $a$, $b$, and $c$ in a linear order such that $a \leq b \leq c$, the union of the half-open intervals $[a, b)$ and $[b, c)$ is equal to the half-open interval $[a, c)$.

Set.Ico_union_Ico' theorem

(h₁ : c ≤ b) (h₂ : a ≤ d) : Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Full source

theorem Ico_union_Ico' (h₁ : c ≤ b) (h₂ : a ≤ d) : IcoIco a b ∪ Ico c d = Ico (min a c) (max b d) := by
  ext1 x
  simp_rw [mem_union, mem_Ico, min_le_iff, lt_max_iff]
  by_cases hc : c ≤ x <;> by_cases hd : x < d
  · tauto
  · have hax : a ≤ x := h₂.trans (le_of_not_gt hd)
    tauto
  · have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
    tauto
  · tauto

Union of Two Half-Open Intervals Under Order Conditions

Informal description

For any elements $a, b, c, d$ in a linear order, if $c \leq b$ and $a \leq d$, then the union of the half-open intervals $[a, b)$ and $[c, d)$ is equal to the half-open interval $[\min(a, c), \max(b, d))$.

Set.Ico_union_Ico theorem

(h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) : Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Full source

theorem Ico_union_Ico (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
    IcoIco a b ∪ Ico c d = Ico (min a c) (max b d) := by
  rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd <;> simp [*] at h₁ h₂
  · exact Ico_union_Ico' h₂ h₁
  all_goals simp [*]

Union of Two Half-Open Intervals Under Overlap Conditions

Informal description

For any elements $a, b, c, d$ in a linear order, if $\min(a, b) \leq \max(c, d)$ and $\min(c, d) \leq \max(a, b)$, then the union of the half-open intervals $[a, b)$ and $[c, d)$ is equal to the half-open interval $[\min(a, c), \max(b, d))$.

Set.Icc_subset_Ico_union_Icc theorem

: Icc a c ⊆ Ico a b ∪ Icc b c

Full source

theorem Icc_subset_Ico_union_Icc : IccIcc a c ⊆ Ico a b ∪ Icc b c := fun x hx =>
  (lt_or_le x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Inclusion of Closed Interval in Union of Half-Open and Closed Intervals

Informal description

For any elements $a \leq b \leq c$ in a linear order, the closed interval $[a, c]$ is contained in the union of the half-open interval $[a, b)$ and the closed interval $[b, c]$.

Set.Ico_union_Icc_eq_Icc theorem

(h₁ : a ≤ b) (h₂ : b ≤ c) : Ico a b ∪ Icc b c = Icc a c

Full source

@[simp]
theorem Ico_union_Icc_eq_Icc (h₁ : a ≤ b) (h₂ : b ≤ c) : IcoIco a b ∪ Icc b c = Icc a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.le.trans h₂⟩) fun hx => ⟨h₁.trans hx.1, hx.2⟩)
    Icc_subset_Ico_union_Icc

Union of Half-Open and Closed Intervals Equals Closed Interval

Informal description

For any elements $a \leq b \leq c$ in a linear order, the union of the half-open interval $[a, b)$ and the closed interval $[b, c]$ equals the closed interval $[a, c]$.

Set.Ioc_subset_Ioo_union_Icc theorem

: Ioc a c ⊆ Ioo a b ∪ Icc b c

Full source

theorem Ioc_subset_Ioo_union_Icc : IocIoc a c ⊆ Ioo a b ∪ Icc b c := fun x hx =>
  (lt_or_le x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Inclusion of Right-Open Interval in Union of Open and Closed Intervals

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the right-open interval $(a, c]$ is a subset of the union of the open interval $(a, b)$ and the closed interval $[b, c]$.

Set.Ioo_union_Icc_eq_Ioc theorem

(h₁ : a < b) (h₂ : b ≤ c) : Ioo a b ∪ Icc b c = Ioc a c

Full source

@[simp]
theorem Ioo_union_Icc_eq_Ioc (h₁ : a < b) (h₂ : b ≤ c) : IooIoo a b ∪ Icc b c = Ioc a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.le.trans h₂⟩) fun hx => ⟨h₁.trans_le hx.1, hx.2⟩)
    Ioc_subset_Ioo_union_Icc

Union of Open and Closed Intervals Equals Right-Open Interval under Order Conditions

Informal description

For any elements $a$, $b$, and $c$ in a linear order such that $a < b$ and $b \leq c$, the union of the open interval $(a, b)$ and the closed interval $[b, c]$ equals the right-open interval $(a, c]$.

Set.Ioo_subset_Ioc_union_Ioo theorem

: Ioo a c ⊆ Ioc a b ∪ Ioo b c

Full source

theorem Ioo_subset_Ioc_union_Ioo : IooIoo a c ⊆ Ioc a b ∪ Ioo b c := fun x hx =>
  (le_or_lt x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Inclusion of Open Interval in Union of Half-Open and Open Intervals

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the open interval $(a, c)$ is a subset of the union of the half-open interval $(a, b]$ and the open interval $(b, c)$. In other words, $(a, c) \subseteq (a, b] \cup (b, c)$.

Set.Ioc_union_Ioo_eq_Ioo theorem

(h₁ : a ≤ b) (h₂ : b < c) : Ioc a b ∪ Ioo b c = Ioo a c

Full source

@[simp]
theorem Ioc_union_Ioo_eq_Ioo (h₁ : a ≤ b) (h₂ : b < c) : IocIoc a b ∪ Ioo b c = Ioo a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans_lt h₂⟩) fun hx => ⟨h₁.trans_lt hx.1, hx.2⟩)
    Ioo_subset_Ioc_union_Ioo

Union of Half-Open and Open Intervals Equals Open Interval: $(a, b] \cup (b, c) = (a, c)$

Informal description

For any elements $a$, $b$, and $c$ in a linear order such that $a \leq b$ and $b < c$, the union of the half-open interval $(a, b]$ and the open interval $(b, c)$ equals the open interval $(a, c)$. That is, $(a, b] \cup (b, c) = (a, c)$.

Set.Ico_subset_Icc_union_Ioo theorem

: Ico a c ⊆ Icc a b ∪ Ioo b c

Full source

theorem Ico_subset_Icc_union_Ioo : IcoIco a c ⊆ Icc a b ∪ Ioo b c := fun x hx =>
  (le_or_lt x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Inclusion of Half-Open Interval in Union of Closed and Open Intervals

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the half-open interval $[a, c)$ is contained in the union of the closed interval $[a, b]$ and the open interval $(b, c)$. That is, $[a, c) \subseteq [a, b] \cup (b, c)$.

Set.Icc_union_Ioo_eq_Ico theorem

(h₁ : a ≤ b) (h₂ : b < c) : Icc a b ∪ Ioo b c = Ico a c

Full source

@[simp]
theorem Icc_union_Ioo_eq_Ico (h₁ : a ≤ b) (h₂ : b < c) : IccIcc a b ∪ Ioo b c = Ico a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans_lt h₂⟩) fun hx => ⟨h₁.trans hx.1.le, hx.2⟩)
    Ico_subset_Icc_union_Ioo

Union of Closed and Open Intervals Equals Half-Open Interval

Informal description

For any elements $a$, $b$, and $c$ in a linear order such that $a \leq b$ and $b < c$, the union of the closed interval $[a, b]$ and the open interval $(b, c)$ equals the half-open interval $[a, c)$. That is, $[a, b] \cup (b, c) = [a, c)$.

Set.Icc_subset_Icc_union_Ioc theorem

: Icc a c ⊆ Icc a b ∪ Ioc b c

Full source

theorem Icc_subset_Icc_union_Ioc : IccIcc a c ⊆ Icc a b ∪ Ioc b c := fun x hx =>
  (le_or_lt x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Inclusion of Closed Interval in Union of Closed and Right-Open Intervals

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the closed interval $[a, c]$ is a subset of the union of the closed interval $[a, b]$ and the right-open interval $(b, c]$.

Set.Icc_union_Ioc_eq_Icc theorem

(h₁ : a ≤ b) (h₂ : b ≤ c) : Icc a b ∪ Ioc b c = Icc a c

Full source

@[simp]
theorem Icc_union_Ioc_eq_Icc (h₁ : a ≤ b) (h₂ : b ≤ c) : IccIcc a b ∪ Ioc b c = Icc a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans h₂⟩) fun hx => ⟨h₁.trans hx.1.le, hx.2⟩)
    Icc_subset_Icc_union_Ioc

Union of Closed and Right-Open Intervals Equals Closed Interval

Informal description

For any elements $a$, $b$, and $c$ in a linear order such that $a \leq b$ and $b \leq c$, the union of the closed interval $[a, b]$ and the right-open interval $(b, c]$ equals the closed interval $[a, c]$, i.e., $[a, b] \cup (b, c] = [a, c]$.

Set.Ioc_subset_Ioc_union_Ioc theorem

: Ioc a c ⊆ Ioc a b ∪ Ioc b c

Full source

theorem Ioc_subset_Ioc_union_Ioc : IocIoc a c ⊆ Ioc a b ∪ Ioc b c := fun x hx =>
  (le_or_lt x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

Inclusion of Open-Closed Interval in Union of Two Open-Closed Intervals

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the open-closed interval $(a, c]$ is contained in the union of the open-closed intervals $(a, b]$ and $(b, c]$.

Set.Ioc_union_Ioc_eq_Ioc theorem

(h₁ : a ≤ b) (h₂ : b ≤ c) : Ioc a b ∪ Ioc b c = Ioc a c

Full source

@[simp]
theorem Ioc_union_Ioc_eq_Ioc (h₁ : a ≤ b) (h₂ : b ≤ c) : IocIoc a b ∪ Ioc b c = Ioc a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans h₂⟩) fun hx => ⟨h₁.trans_lt hx.1, hx.2⟩)
    Ioc_subset_Ioc_union_Ioc

Union of Adjacent Open-Closed Intervals Equals Larger Open-Closed Interval

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set such that $a \leq b$ and $b \leq c$, the union of the open-closed intervals $(a, b]$ and $(b, c]$ is equal to the open-closed interval $(a, c]$.

Set.Ioc_union_Ioc' theorem

(h₁ : c ≤ b) (h₂ : a ≤ d) : Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)

Full source

theorem Ioc_union_Ioc' (h₁ : c ≤ b) (h₂ : a ≤ d) : IocIoc a b ∪ Ioc c d = Ioc (min a c) (max b d) := by
  ext1 x
  simp_rw [mem_union, mem_Ioc, min_lt_iff, le_max_iff]
  by_cases hc : c < x <;> by_cases hd : x ≤ d
  · tauto
  · have hax : a < x := h₂.trans_lt (lt_of_not_ge hd)
    tauto
  · have hxb : x ≤ b := (le_of_not_gt hc).trans h₁
    tauto
  · tauto

Union of Two Open-Closed Intervals Under Order Conditions

Informal description

For any elements $a$, $b$, $c$, and $d$ in a linearly ordered set, if $c \leq b$ and $a \leq d$, then the union of the open-closed intervals $(a, b]$ and $(c, d]$ is equal to the open-closed interval $(\min(a, c), \max(b, d)]$.

Set.Ioc_union_Ioc theorem

(h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) : Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)

Full source

theorem Ioc_union_Ioc (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
    IocIoc a b ∪ Ioc c d = Ioc (min a c) (max b d) := by
  rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd <;> simp [*] at h₁ h₂
  · exact Ioc_union_Ioc' h₂ h₁
  all_goals simp [*]

Union of Two Open-Closed Intervals Under Overlap Conditions

Informal description

For any elements $a$, $b$, $c$, and $d$ in a linearly ordered set, if $\min(a, b) \leq \max(c, d)$ and $\min(c, d) \leq \max(a, b)$, then the union of the open-closed intervals $(a, b]$ and $(c, d]$ is equal to the open-closed interval $(\min(a, c), \max(b, d)]$.

Set.Ioo_subset_Ioc_union_Ico theorem

: Ioo a c ⊆ Ioc a b ∪ Ico b c

Full source

theorem Ioo_subset_Ioc_union_Ico : IooIoo a c ⊆ Ioc a b ∪ Ico b c :=
  Subset.trans Ioo_subset_Ioc_union_Ioo (union_subset_union_right _ Ioo_subset_Ico_self)

Inclusion of Open Interval in Union of Half-Open and Closed-Open Intervals

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the open interval $(a, c)$ is a subset of the union of the half-open interval $(a, b]$ and the closed-open interval $[b, c)$. In other words, $(a, c) \subseteq (a, b] \cup [b, c)$.

Set.Ioc_union_Ico_eq_Ioo theorem

(h₁ : a < b) (h₂ : b < c) : Ioc a b ∪ Ico b c = Ioo a c

Full source

@[simp]
theorem Ioc_union_Ico_eq_Ioo (h₁ : a < b) (h₂ : b < c) : IocIoc a b ∪ Ico b c = Ioo a c :=
  Subset.antisymm
    (fun _ hx =>
      hx.elim (fun hx' => ⟨hx'.1, hx'.2.trans_lt h₂⟩) fun hx' => ⟨h₁.trans_le hx'.1, hx'.2⟩)
    Ioo_subset_Ioc_union_Ico

Union of Half-Open and Closed-Open Intervals Equals Open Interval Under Strict Ordering

Informal description

For any elements $a$, $b$, and $c$ in a linear order such that $a < b$ and $b < c$, the union of the half-open interval $(a, b]$ and the closed-open interval $[b, c)$ equals the open interval $(a, c)$. That is, $(a, b] \cup [b, c) = (a, c)$.

Set.Ico_subset_Icc_union_Ico theorem

: Ico a c ⊆ Icc a b ∪ Ico b c

Full source

theorem Ico_subset_Icc_union_Ico : IcoIco a c ⊆ Icc a b ∪ Ico b c :=
  Subset.trans Ico_subset_Icc_union_Ioo (union_subset_union_right _ Ioo_subset_Ico_self)

Inclusion of Half-Open Interval in Union of Closed and Half-Open Intervals

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the half-open interval $[a, c)$ is contained in the union of the closed interval $[a, b]$ and the half-open interval $[b, c)$. That is, $[a, c) \subseteq [a, b] \cup [b, c)$.

Set.Icc_union_Ico_eq_Ico theorem

(h₁ : a ≤ b) (h₂ : b < c) : Icc a b ∪ Ico b c = Ico a c

Full source

@[simp]
theorem Icc_union_Ico_eq_Ico (h₁ : a ≤ b) (h₂ : b < c) : IccIcc a b ∪ Ico b c = Ico a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans_lt h₂⟩) fun hx => ⟨h₁.trans hx.1, hx.2⟩)
    Ico_subset_Icc_union_Ico

Union of Closed and Half-Open Intervals Equals Half-Open Interval Under Ordering Conditions

Informal description

For any elements $a$, $b$, and $c$ in a linear order such that $a \leq b$ and $b < c$, the union of the closed interval $[a, b]$ and the half-open interval $[b, c)$ equals the half-open interval $[a, c)$. That is, $[a, b] \cup [b, c) = [a, c)$.

Set.Icc_subset_Icc_union_Icc theorem

: Icc a c ⊆ Icc a b ∪ Icc b c

Full source

theorem Icc_subset_Icc_union_Icc : IccIcc a c ⊆ Icc a b ∪ Icc b c :=
  Subset.trans Icc_subset_Icc_union_Ioc (union_subset_union_right _ Ioc_subset_Icc_self)

Closed Interval Subset of Union of Two Closed Intervals

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the closed interval $[a, c]$ is a subset of the union of the closed intervals $[a, b]$ and $[b, c]$.

Set.Icc_union_Icc_eq_Icc theorem

(h₁ : a ≤ b) (h₂ : b ≤ c) : Icc a b ∪ Icc b c = Icc a c

Full source

@[simp]
theorem Icc_union_Icc_eq_Icc (h₁ : a ≤ b) (h₂ : b ≤ c) : IccIcc a b ∪ Icc b c = Icc a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans h₂⟩) fun hx => ⟨h₁.trans hx.1, hx.2⟩)
    Icc_subset_Icc_union_Icc

Union of Adjacent Closed Intervals in a Linear Order

Informal description

For any elements $a$, $b$, and $c$ in a linear order such that $a \leq b$ and $b \leq c$, the union of the closed intervals $[a, b]$ and $[b, c]$ is equal to the closed interval $[a, c]$.

Set.Icc_union_Icc' theorem

(h₁ : c ≤ b) (h₂ : a ≤ d) : Icc a b ∪ Icc c d = Icc (min a c) (max b d)

Full source

theorem Icc_union_Icc' (h₁ : c ≤ b) (h₂ : a ≤ d) : IccIcc a b ∪ Icc c d = Icc (min a c) (max b d) := by
  ext1 x
  simp_rw [mem_union, mem_Icc, min_le_iff, le_max_iff]
  by_cases hc : c ≤ x <;> by_cases hd : x ≤ d
  · tauto
  · have hax : a ≤ x := h₂.trans (le_of_not_ge hd)
    tauto
  · have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
    tauto
  · tauto

Union of Two Closed Intervals in a Linear Order

Informal description

For any elements $a, b, c, d$ in a linear order, if $c \leq b$ and $a \leq d$, then the union of the closed intervals $[a, b]$ and $[c, d]$ is equal to the closed interval $[\min(a, c), \max(b, d)]$.

Set.Icc_union_Icc theorem

(h₁ : min a b < max c d) (h₂ : min c d < max a b) : Icc a b ∪ Icc c d = Icc (min a c) (max b d)

Full source

/-- We cannot replace `<` by `≤` in the hypotheses.
Otherwise for `b < a = d < c` the l.h.s. is `∅` and the r.h.s. is `{a}`.
-/
theorem Icc_union_Icc (h₁ : min a b < max c d) (h₂ : min c d < max a b) :
    IccIcc a b ∪ Icc c d = Icc (min a c) (max b d) := by
  rcases le_or_lt a b with hab | hab <;> rcases le_or_lt c d with hcd | hcd <;>
    simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt,
      min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂
  · exact Icc_union_Icc' h₂.le h₁.le
  all_goals simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]

Union of Two Overlapping Closed Intervals in a Linear Order

Informal description

For any elements $a, b, c, d$ in a linear order, if $\min(a, b) < \max(c, d)$ and $\min(c, d) < \max(a, b)$, then the union of the closed intervals $[a, b]$ and $[c, d]$ is equal to the closed interval $[\min(a, c), \max(b, d)]$.

Set.Ioc_subset_Ioc_union_Icc theorem

: Ioc a c ⊆ Ioc a b ∪ Icc b c

Full source

theorem Ioc_subset_Ioc_union_Icc : IocIoc a c ⊆ Ioc a b ∪ Icc b c :=
  Subset.trans Ioc_subset_Ioc_union_Ioc (union_subset_union_right _ Ioc_subset_Icc_self)

Inclusion of $(a, c]$ in $(a, b] \cup [b, c]$ in Linear Orders

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the open-closed interval $(a, c]$ is contained in the union of the open-closed interval $(a, b]$ and the closed interval $[b, c]$.

Set.Ioc_union_Icc_eq_Ioc theorem

(h₁ : a < b) (h₂ : b ≤ c) : Ioc a b ∪ Icc b c = Ioc a c

Full source

@[simp]
theorem Ioc_union_Icc_eq_Ioc (h₁ : a < b) (h₂ : b ≤ c) : IocIoc a b ∪ Icc b c = Ioc a c :=
  Subset.antisymm
    (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans h₂⟩) fun hx => ⟨h₁.trans_le hx.1, hx.2⟩)
    Ioc_subset_Ioc_union_Icc

Union of Adjacent Open-Closed and Closed Intervals in Linear Order

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set such that $a < b$ and $b \leq c$, the union of the open-closed interval $(a, b]$ and the closed interval $[b, c]$ equals the open-closed interval $(a, c]$, i.e., $$(a, b] \cup [b, c] = (a, c].$$

Set.Ioo_union_Ioo' theorem

(h₁ : c < b) (h₂ : a < d) : Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)

Full source

theorem Ioo_union_Ioo' (h₁ : c < b) (h₂ : a < d) : IooIoo a b ∪ Ioo c d = Ioo (min a c) (max b d) := by
  ext1 x
  simp_rw [mem_union, mem_Ioo, min_lt_iff, lt_max_iff]
  by_cases hc : c < x <;> by_cases hd : x < d
  · tauto
  · have hax : a < x := h₂.trans_le (le_of_not_lt hd)
    tauto
  · have hxb : x < b := (le_of_not_lt hc).trans_lt h₁
    tauto
  · tauto

Union of Two Overlapping Open Intervals

Informal description

For real numbers $a, b, c, d$ with $c < b$ and $a < d$, the union of the open intervals $(a, b)$ and $(c, d)$ equals the open interval from $\min(a, c)$ to $\max(b, d)$, i.e., $$(a, b) \cup (c, d) = (\min(a, c), \max(b, d)).$$

Set.Ioo_union_Ioo theorem

(h₁ : min a b < max c d) (h₂ : min c d < max a b) : Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)

Full source

theorem Ioo_union_Ioo (h₁ : min a b < max c d) (h₂ : min c d < max a b) :
    IooIoo a b ∪ Ioo c d = Ioo (min a c) (max b d) := by
  rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd <;>
    simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂
  · exact Ioo_union_Ioo' h₂ h₁
  all_goals
    simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt,
      le_of_lt h₂, le_of_lt h₁]

Union of Two Overlapping Open Intervals in Linear Order

Informal description

For any elements $a, b, c, d$ in a linear order, if $\min(a, b) < \max(c, d)$ and $\min(c, d) < \max(a, b)$, then the union of the open intervals $(a, b)$ and $(c, d)$ equals the open interval from $\min(a, c)$ to $\max(b, d)$, i.e., $$(a, b) \cup (c, d) = (\min(a, c), \max(b, d)).$$

Set.Ioo_subset_Ioo_union_Ioo theorem

(h₁ : a ≤ a₁) (h₂ : c < b) (h₃ : b₁ ≤ d) : Ioo a₁ b₁ ⊆ Ioo a b ∪ Ioo c d

Full source

theorem Ioo_subset_Ioo_union_Ioo (h₁ : a ≤ a₁) (h₂ : c < b) (h₃ : b₁ ≤ d) :
    IooIoo a₁ b₁ ⊆ Ioo a b ∪ Ioo c d := fun x hx =>
  (lt_or_le x b).elim (fun hxb => Or.inl ⟨lt_of_le_of_lt h₁ hx.1, hxb⟩)
    fun hxb => Or.inr ⟨lt_of_lt_of_le h₂ hxb, lt_of_lt_of_le hx.2 h₃⟩

Inclusion of Open Interval in Union of Two Open Intervals

Informal description

For any elements $a, a_1, b, b_1, c, d$ in a linear order, if $a \leq a_1$, $c < b$, and $b_1 \leq d$, then the open interval $(a_1, b_1)$ is contained in the union of the open intervals $(a, b)$ and $(c, d)$.

Set.Ioi_inter_Ioi theorem

: Ioi a ∩ Ioi b = Ioi (a ⊔ b)

Full source

@[simp]
theorem Ioi_inter_Ioi : IoiIoi a ∩ Ioi b = Ioi (a ⊔ b) :=
  ext fun _ => sup_lt_iff.symm

Intersection of Right Open Intervals: $(a, \infty) \cap (b, \infty) = (\max(a, b), \infty)$

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the intersection of the open right intervals $(a, \infty)$ and $(b, \infty)$ is equal to the open right interval $(\max(a, b), \infty)$.

Set.Iio_inter_Iio theorem

: Iio a ∩ Iio b = Iio (a ⊓ b)

Full source

@[simp]
theorem Iio_inter_Iio : IioIio a ∩ Iio b = Iio (a ⊓ b) :=
  ext fun _ => lt_inf_iff.symm

Intersection of Two Left-Infinite Open Intervals is Left-Infinite Open Interval up to Minimum

Informal description

For any elements $a$ and $b$ in a linear order, the intersection of the open intervals $(-\infty, a)$ and $(-\infty, b)$ is equal to the open interval $(-\infty, \min(a, b))$. In symbols: \[ (-\infty, a) \cap (-\infty, b) = (-\infty, \min(a, b)). \]

Set.Ico_inter_Ico theorem

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

Full source

theorem Ico_inter_Ico : IcoIco a₁ b₁ ∩ Ico a₂ b₂ = Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂) := by
  simp only [Ici_inter_Iio.symm, Ici_inter_Ici.symm, Iio_inter_Iio.symm]; ac_rfl

Intersection of Half-Open Intervals: $[a₁, b₁) \cap [a₂, b₂) = [\max(a₁, a₂), \min(b₁, b₂))$

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a linear order, the intersection of the half-open intervals $[a₁, b₁)$ and $[a₂, b₂)$ is equal to the half-open interval $[\max(a₁, a₂), \min(b₁, b₂))$. In symbols: \[ [a₁, b₁) \cap [a₂, b₂) = [\max(a₁, a₂), \min(b₁, b₂)). \]

Set.Ioc_inter_Ioc theorem

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

Full source

theorem Ioc_inter_Ioc : IocIoc a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂) := by
  simp only [Ioi_inter_Iic.symm, Ioi_inter_Ioi.symm, Iic_inter_Iic.symm]; ac_rfl

Intersection of Right-Open Left-Closed Intervals: $(a₁, b₁] \cap (a₂, b₂] = (\max(a₁, a₂), \min(b₁, b₂)]$

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a linearly ordered set, the intersection of the right-open left-closed intervals $(a₁, b₁]$ and $(a₂, b₂]$ is equal to the right-open left-closed interval $(\max(a₁, a₂), \min(b₁, b₂)]$. In symbols: \[ (a₁, b₁] \cap (a₂, b₂] = (\max(a₁, a₂), \min(b₁, b₂)]. \]

Set.Ioo_inter_Ioo theorem

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

Full source

theorem Ioo_inter_Ioo : IooIoo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (a₁ ⊔ a₂) (b₁ ⊓ b₂) := by
  simp only [Ioi_inter_Iio.symm, Ioi_inter_Ioi.symm, Iio_inter_Iio.symm]; ac_rfl

Intersection of Open Intervals: $(a₁, b₁) \cap (a₂, b₂) = (\max(a₁, a₂), \min(b₁, b₂))$

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a linearly ordered set, the intersection of the open intervals $(a₁, b₁)$ and $(a₂, b₂)$ is equal to the open interval $(\max(a₁, a₂), \min(b₁, b₂))$. In symbols: \[ (a₁, b₁) \cap (a₂, b₂) = (\max(a₁, a₂), \min(b₁, b₂)). \]

Set.Ioo_inter_Iio theorem

: Ioo a b ∩ Iio c = Ioo a (min b c)

Full source

theorem Ioo_inter_Iio : IooIoo a b ∩ Iio c = Ioo a (min b c) := by
  ext
  simp_rw [mem_inter_iff, mem_Ioo, mem_Iio, lt_min_iff, and_assoc]

Intersection of Open Interval with Left-Infinite Open Interval: $(a, b) \cap (-\infty, c) = (a, \min(b, c))$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the intersection of the open interval $(a, b)$ and the left-infinite open interval $(-\infty, c)$ is equal to the open interval $(a, \min(b, c))$.

Set.Iio_inter_Ioo theorem

: Iio a ∩ Ioo b c = Ioo b (min a c)

Full source

theorem Iio_inter_Ioo : IioIio a ∩ Ioo b c = Ioo b (min a c) := by
  rw [Set.inter_comm, Set.Ioo_inter_Iio, min_comm]

Intersection of Left-Infinite Open Interval with Open Interval: $(-\infty, a) \cap (b, c) = (b, \min(a, c))$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the intersection of the left-infinite open interval $(-\infty, a)$ and the open interval $(b, c)$ is equal to the open interval $(b, \min(a, c))$.

Set.Ioo_inter_Ioi theorem

: Ioo a b ∩ Ioi c = Ioo (max a c) b

Full source

theorem Ioo_inter_Ioi : IooIoo a b ∩ Ioi c = Ioo (max a c) b := by
  ext
  simp_rw [mem_inter_iff, mem_Ioo, mem_Ioi, max_lt_iff, and_assoc, and_comm]

Intersection of Open Interval with Open Ray in Linear Order

Informal description

For any elements $a, b, c$ in a linear order, the intersection of the open interval $(a, b)$ with the open ray $(c, \infty)$ is the open interval $(\max(a, c), b)$. That is, $$(a, b) \cap (c, \infty) = (\max(a, c), b).$$

Set.Ioi_inter_Ioo theorem

: Set.Ioi a ∩ Set.Ioo b c = Set.Ioo (max a b) c

Full source

theorem Ioi_inter_Ioo : Set.IoiSet.Ioi a ∩ Set.Ioo b c = Set.Ioo (max a b) c := by
  rw [inter_comm, Ioo_inter_Ioi, max_comm]

Intersection of Open Ray with Open Interval: $(a, \infty) \cap (b, c) = (\max(a, b), c)$

Informal description

For any elements $a, b, c$ in a linear order, the intersection of the open ray $(a, \infty)$ with the open interval $(b, c)$ is the open interval $(\max(a, b), c)$. That is, $$(a, \infty) \cap (b, c) = (\max(a, b), c).$$

Set.Ioc_inter_Ioo_of_left_lt theorem

(h : b₁ < b₂) : Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioc (max a₁ a₂) b₁

Full source

theorem Ioc_inter_Ioo_of_left_lt (h : b₁ < b₂) : IocIoc a₁ b₁ ∩ Ioo a₂ b₂ = Ioc (max a₁ a₂) b₁ :=
  ext fun x => by
    simp [and_assoc, @and_left_comm (x ≤ _), and_iff_left_iff_imp.2 fun h' => lt_of_le_of_lt h' h]

Intersection of Half-Open and Open Intervals when $b₁ < b₂$: $(a₁, b₁] \cap (a₂, b₂) = (\max(a₁, a₂), b₁]$

Informal description

For real numbers $a₁, a₂, b₁, b₂$ with $b₁ < b₂$, the intersection of the half-open interval $(a₁, b₁]$ and the open interval $(a₂, b₂)$ is equal to the half-open interval $(\max(a₁, a₂), b₁]$.

Set.Ioc_inter_Ioo_of_right_le theorem

(h : b₂ ≤ b₁) : Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) b₂

Full source

theorem Ioc_inter_Ioo_of_right_le (h : b₂ ≤ b₁) : IocIoc a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) b₂ :=
  ext fun x => by
    simp [and_assoc, @and_left_comm (x ≤ _),
      and_iff_right_iff_imp.2 fun h' => (le_of_lt h').trans h]

Intersection of Half-Open and Open Intervals with Right Endpoint Condition

Informal description

For any real numbers $a₁, a₂, b₁, b₂$ with $b₂ \leq b₁$, the intersection of the half-open interval $(a₁, b₁]$ and the open interval $(a₂, b₂)$ is equal to the open interval $(\max(a₁, a₂), b₂)$.

Set.Ioo_inter_Ioc_of_left_le theorem

(h : b₁ ≤ b₂) : Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁

Full source

theorem Ioo_inter_Ioc_of_left_le (h : b₁ ≤ b₂) : IooIoo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁ := by
  rw [inter_comm, Ioc_inter_Ioo_of_right_le h, max_comm]

Intersection of Open and Half-Open Intervals when $b₁ \leq b₂$: $(a₁, b₁) \cap (a₂, b₂] = (\max(a₁, a₂), b₁)$

Informal description

For any real numbers $a₁, a₂, b₁, b₂$ with $b₁ \leq b₂$, the intersection of the open interval $(a₁, b₁)$ and the half-open interval $(a₂, b₂]$ is equal to the open interval $(\max(a₁, a₂), b₁)$.

Set.Ioo_inter_Ioc_of_right_lt theorem

(h : b₂ < b₁) : Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂

Full source

theorem Ioo_inter_Ioc_of_right_lt (h : b₂ < b₁) : IooIoo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂ := by
  rw [inter_comm, Ioc_inter_Ioo_of_left_lt h, max_comm]

Intersection of Open and Half-Open Intervals when $b₂ < b₁$: $(a₁, b₁) \cap (a₂, b₂] = (\max(a₁, a₂), b₂]$

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a linear order with $b₂ < b₁$, the intersection of the open interval $(a₁, b₁)$ and the half-open interval $(a₂, b₂]$ is equal to the half-open interval $(\max(a₁, a₂), b₂]$.

Set.Ico_diff_Iio theorem

: Ico a b \ Iio c = Ico (max a c) b

Full source

@[simp]
theorem Ico_diff_Iio : IcoIco a b \ Iio c = Ico (max a c) b := by
  rw [diff_eq, compl_Iio, Ico_inter_Ici]

Difference of Half-Closed Interval and Left-Infinite Open Interval: $[a, b) \setminus (-\infty, c) = [\max(a, c), b)$

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the set difference between the half-closed interval $[a, b)$ and the left-infinite open interval $(-\infty, c)$ is equal to the half-closed interval $[\max(a, c), b)$. In symbols: $$ [a, b) \setminus (-\infty, c) = [\max(a, c), b). $$

Set.Ioc_diff_Ioi theorem

: Ioc a b \ Ioi c = Ioc a (min b c)

Full source

@[simp]
theorem Ioc_diff_Ioi : IocIoc a b \ Ioi c = Ioc a (min b c) :=
  ext <| by simp +contextual [iff_def]

Difference of Half-Open Interval and Open Ray in Linear Order

Informal description

For any elements $a$, $b$, and $c$ in a linear order, the set difference between the half-open interval $(a, b]$ and the open ray $(c, \infty)$ is equal to the half-open interval $(a, \min(b, c)]$. In symbols: $$ (a, b] \setminus (c, \infty) = (a, \min(b, c)]. $$

Set.Ioc_inter_Ioi theorem

: Ioc a b ∩ Ioi c = Ioc (a ⊔ c) b

Full source

@[simp]
theorem Ioc_inter_Ioi : IocIoc a b ∩ Ioi c = Ioc (a ⊔ c) b := by
  rw [← Ioi_inter_Iic, inter_assoc, inter_comm, inter_assoc, Ioi_inter_Ioi, inter_comm,
    Ioi_inter_Iic, sup_comm]

Intersection of Half-Open and Right Open Intervals: $(a, b] \cap (c, \infty) = (\max(a, c), b]$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the intersection of the half-open interval $(a, b]$ and the open right interval $(c, \infty)$ is equal to the half-open interval $(\max(a, c), b]$. In symbols: $$ (a, b] \cap (c, \infty) = (\max(a, c), b]. $$

Set.Ico_inter_Iio theorem

: Ico a b ∩ Iio c = Ico a (min b c)

Full source

@[simp]
theorem Ico_inter_Iio : IcoIco a b ∩ Iio c = Ico a (min b c) :=
  ext <| by simp +contextual [iff_def]

Intersection of Half-Open and Open Intervals in Linear Order

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the intersection of the half-open interval $[a, b)$ and the open interval $(-\infty, c)$ is equal to the half-open interval $[a, \min(b, c))$. In symbols: \[ [a, b) \cap (-\infty, c) = [a, \min(b, c)). \]

Set.Ioc_diff_Iic theorem

: Ioc a b \ Iic c = Ioc (max a c) b

Full source

@[simp]
theorem Ioc_diff_Iic : IocIoc a b \ Iic c = Ioc (max a c) b := by
  rw [diff_eq, compl_Iic, Ioc_inter_Ioi]

Difference of Half-Open and Closed Intervals: $(a, b] \setminus (-\infty, c] = (\max(a, c), b]$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the set difference between the half-open interval $(a, b]$ and the closed interval $(-\infty, c]$ is equal to the half-open interval $(\max(a, c), b]$. In symbols: $$ (a, b] \setminus (-\infty, c] = (\max(a, c), b]. $$

Set.compl_Ioc theorem

: (Ioc a b)ᶜ = Iic a ∪ Ioi b

Full source

theorem compl_Ioc : (Ioc a b)ᶜ = IicIic a ∪ Ioi b := by
  ext i
  rw [mem_compl_iff, mem_Ioc, mem_union, mem_Iic, mem_Ioi, not_and_or, not_lt, not_le]

Complement of Open-Closed Interval Equals Union of Closed and Open Intervals

Informal description

The complement of the open-closed interval $(a, b]$ in a linear order is equal to the union of the closed interval $(-\infty, a]$ and the open interval $(b, \infty)$, i.e., $(a, b]^c = (-\infty, a] \cup (b, \infty)$.

Set.Iic_diff_Ioc theorem

: Iic b \ Ioc a b = Iic (a ⊓ b)

Full source

theorem Iic_diff_Ioc : IicIic b \ Ioc a b = Iic (a ⊓ b) := by
  rw [diff_eq, compl_Ioc, inter_union_distrib_left, Iic_inter_Iic, ← compl_Iic, inter_compl_self,
    union_empty, min_comm]

Difference of Closed and Open-Closed Intervals Equals Closed Interval to Infimum

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the set difference between the closed interval $(-\infty, b]$ and the open-closed interval $(a, b]$ is equal to the closed interval $(-\infty, a \sqcap b]$, where $\sqcap$ denotes the infimum (meet) of $a$ and $b$.

Set.Iic_diff_Ioc_self_of_le theorem

(hab : a ≤ b) : Iic b \ Ioc a b = Iic a

Full source

theorem Iic_diff_Ioc_self_of_le (hab : a ≤ b) : IicIic b \ Ioc a b = Iic a := by
  rw [Iic_diff_Ioc, min_eq_left hab]

Difference of Closed and Open-Closed Intervals under Inequality: $(-\infty, b] \setminus (a, b] = (-\infty, a]$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a linearly ordered set such that $a \leq b$, the set difference between the closed interval $(-\infty, b]$ and the open-closed interval $(a, b]$ is equal to the closed interval $(-\infty, a]$.

Set.Ioc_union_Ioc_right theorem

: Ioc a b ∪ Ioc a c = Ioc a (max b c)

Full source

@[simp]
theorem Ioc_union_Ioc_right : IocIoc a b ∪ Ioc a c = Ioc a (max b c) := by
  rw [Ioc_union_Ioc, min_self] <;> exact (min_le_left _ _).trans (le_max_left _ _)

Union of Open-Closed Intervals with Common Left Endpoint: $(a, b] \cup (a, c] = (a, \max(b, c)]$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the union of the open-closed intervals $(a, b]$ and $(a, c]$ is equal to the open-closed interval $(a, \max(b, c)]$.

Set.Ioc_union_Ioc_left theorem

: Ioc a c ∪ Ioc b c = Ioc (min a b) c

Full source

@[simp]
theorem Ioc_union_Ioc_left : IocIoc a c ∪ Ioc b c = Ioc (min a b) c := by
  rw [Ioc_union_Ioc, max_self] <;> exact (min_le_right _ _).trans (le_max_right _ _)

Union of Two Open-Closed Intervals with Common Right Endpoint

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the union of the open-closed intervals $(a, c]$ and $(b, c]$ is equal to the open-closed interval $(\min(a, b), c]$.

Set.Ioc_union_Ioc_symm theorem

: Ioc a b ∪ Ioc b a = Ioc (min a b) (max a b)

Full source

@[simp]
theorem Ioc_union_Ioc_symm : IocIoc a b ∪ Ioc b a = Ioc (min a b) (max a b) := by
  rw [max_comm]
  apply Ioc_union_Ioc <;> rw [max_comm] <;> exact min_le_max

Symmetric Union of Open-Closed Intervals: $(a, b] \cup (b, a] = (\min(a, b), \max(a, b)]$

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the union of the open-closed intervals $(a, b]$ and $(b, a]$ is equal to the open-closed interval $(\min(a, b), \max(a, b)]$.

Set.Ioc_union_Ioc_union_Ioc_cycle theorem

: Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc (min a (min b c)) (max a (max b c))

Full source

@[simp]
theorem Ioc_union_Ioc_union_Ioc_cycle :
    IocIoc a b ∪ Ioc b cIoc a b ∪ Ioc b c ∪ Ioc c a = Ioc (min a (min b c)) (max a (max b c)) := by
  rw [Ioc_union_Ioc, Ioc_union_Ioc]
  · ac_rfl
  all_goals
  solve_by_elim (config := { maxDepth := 5 }) [min_le_of_left_le, min_le_of_right_le,
       le_max_of_le_left, le_max_of_le_right, le_refl]

Union of Three Cyclic Open-Closed Intervals

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the union of the open-closed intervals $(a, b]$, $(b, c]$, and $(c, a]$ is equal to the open-closed interval $(\min(a, b, c), \max(a, b, c)]$.