Mathlib.Order.Interval.Set.Disjoint

Set.Iic_disjoint_Ioi theorem

(h : a ≤ b) : Disjoint (Iic a) (Ioi b)

Full source

@[simp]
theorem Iic_disjoint_Ioi (h : a ≤ b) : Disjoint (Iic a) (Ioi b) :=
  disjoint_left.mpr fun _ ha hb => (h.trans_lt hb).not_le ha

Disjointness of $(-\infty, a]$ and $(b, \infty)$ for $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ such that $a \leq b$, the left-infinite right-closed interval $(-\infty, a]$ is disjoint from the left-open right-infinite interval $(b, \infty)$.

Set.Iio_disjoint_Ici theorem

(h : a ≤ b) : Disjoint (Iio a) (Ici b)

Full source

@[simp]
theorem Iio_disjoint_Ici (h : a ≤ b) : Disjoint (Iio a) (Ici b) :=
  disjoint_left.mpr fun _ ha hb => (h.trans_lt' ha).not_le hb

Disjointness of $(-\infty, a)$ and $[b, \infty)$ for $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the left-infinite right-open interval $(-\infty, a)$ is disjoint from the left-closed right-infinite interval $[b, \infty)$. In other words, $(-\infty, a) \cap [b, \infty) = \emptyset$.

Set.Iic_disjoint_Ioc theorem

(h : a ≤ b) : Disjoint (Iic a) (Ioc b c)

Full source

@[simp]
theorem Iic_disjoint_Ioc (h : a ≤ b) : Disjoint (Iic a) (Ioc b c) :=
  (Iic_disjoint_Ioi h).mono le_rfl Ioc_subset_Ioi_self

Disjointness of $(-\infty, a]$ and $(b, c]$ for $a \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a preorder $\alpha$ such that $a \leq b$, the left-infinite right-closed interval $(-\infty, a]$ is disjoint from the left-open right-closed interval $(b, c]$.

Set.Ioc_disjoint_Ioc_of_le theorem

{d : α} (h : b ≤ c) : Disjoint (Ioc a b) (Ioc c d)

Full source

@[simp]
theorem Ioc_disjoint_Ioc_of_le {d : α} (h : b ≤ c) : Disjoint (Ioc a b) (Ioc c d) :=
  (Iic_disjoint_Ioc h).mono Ioc_subset_Iic_self le_rfl

Disjointness of Non-overlapping Left-Open Right-Closed Intervals

Informal description

For any elements $a, b, c, d$ in a preorder $\alpha$ such that $b \leq c$, the left-open right-closed intervals $(a, b]$ and $(c, d]$ are disjoint.

Set.Ioc_disjoint_Ioc_same theorem

: Disjoint (Ioc a b) (Ioc b c)

Full source

@[deprecated Ioc_disjoint_Ioc_of_le (since := "2025-03-04")]
theorem Ioc_disjoint_Ioc_same : Disjoint (Ioc a b) (Ioc b c) :=
  (Iic_disjoint_Ioc le_rfl).mono Ioc_subset_Iic_self le_rfl

Disjointness of Adjacent Left-Open Right-Closed Intervals

Informal description

For any elements $a$, $b$, and $c$ in a preorder, the left-open right-closed intervals $(a, b]$ and $(b, c]$ are disjoint.

Set.Ico_disjoint_Ico_same theorem

: Disjoint (Ico a b) (Ico b c)

Full source

@[simp]
theorem Ico_disjoint_Ico_same : Disjoint (Ico a b) (Ico b c) :=
  disjoint_left.mpr fun _ hab hbc => hab.2.not_le hbc.1

Disjointness of Adjacent Left-Closed Right-Open Intervals

Informal description

For any elements $a$, $b$, and $c$ in a preorder, the left-closed right-open intervals $[a, b)$ and $[b, c)$ are disjoint.

Set.Ici_disjoint_Iic theorem

: Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b

Full source

@[simp]
theorem Ici_disjoint_Iic : DisjointDisjoint (Ici a) (Iic b) ↔ ¬a ≤ b := by
  rw [Set.disjoint_iff_inter_eq_empty, Ici_inter_Iic, Icc_eq_empty_iff]

Disjointness of $[a, \infty)$ and $(-\infty, b]$ is equivalent to $\neg (a \leq b)$

Informal description

For any elements $a$ and $b$ in a preorder, the left-closed right-infinite interval $[a, \infty)$ and the left-infinite right-closed interval $(-\infty, b]$ are disjoint if and only if $a$ is not less than or equal to $b$.

Set.Iic_disjoint_Ici theorem

: Disjoint (Iic a) (Ici b) ↔ ¬b ≤ a

Full source

@[simp]
theorem Iic_disjoint_Ici : DisjointDisjoint (Iic a) (Ici b) ↔ ¬b ≤ a :=
  disjoint_comm.trans Ici_disjoint_Iic

Disjointness of $(-\infty, a]$ and $[b, \infty)$ is equivalent to $\neg (b \leq a)$

Informal description

For any elements $a$ and $b$ in a preorder, the left-infinite right-closed interval $(-\infty, a]$ and the left-closed right-infinite interval $[b, \infty)$ are disjoint if and only if $b$ is not less than or equal to $a$.

Set.Ioc_disjoint_Ioi theorem

(h : b ≤ c) : Disjoint (Ioc a b) (Ioi c)

Full source

@[simp]
theorem Ioc_disjoint_Ioi (h : b ≤ c) : Disjoint (Ioc a b) (Ioi c) :=
  disjoint_left.mpr (fun _ hx hy ↦ (hx.2.trans h).not_lt hy)

Disjointness of $(a, b]$ and $(c, \infty)$ when $b \leq c$

Informal description

For any elements $a$, $b$, and $c$ in a preorder $\alpha$, if $b \leq c$, then the left-open right-closed interval $(a, b]$ is disjoint from the left-open right-infinite interval $(c, \infty)$. That is, $(a, b] \cap (c, \infty) = \emptyset$.

Set.Ioc_disjoint_Ioi_same theorem

: Disjoint (Ioc a b) (Ioi b)

Full source

theorem Ioc_disjoint_Ioi_same : Disjoint (Ioc a b) (Ioi b) :=
  Ioc_disjoint_Ioi le_rfl

Disjointness of $(a, b]$ and $(b, \infty)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-open right-closed interval $(a, b]$ is disjoint from the left-open right-infinite interval $(b, \infty)$. That is, $(a, b] \cap (b, \infty) = \emptyset$.

Set.iUnion_Iic theorem

: ⋃ a : α, Iic a = univ

Full source

@[simp]
theorem iUnion_Iic : ⋃ a : α, Iic a = univ :=
  iUnion_eq_univ_iff.2 fun x => ⟨x, right_mem_Iic⟩

Union of Left-Infinite Right-Closed Intervals Covers the Universal Set

Informal description

For any type $\alpha$ with a preorder, the union of all left-infinite right-closed intervals $(-\infty, a]$ over all $a \in \alpha$ is equal to the universal set $\alpha$.

Set.iUnion_Ici theorem

: ⋃ a : α, Ici a = univ

Full source

@[simp]
theorem iUnion_Ici : ⋃ a : α, Ici a = univ :=
  iUnion_eq_univ_iff.2 fun x => ⟨x, left_mem_Ici⟩

Union of All Right-Infinite Closed Intervals Equals Universal Set

Informal description

The union of all left-closed right-infinite intervals $[a, \infty)$ over all elements $a$ in a type $\alpha$ equals the universal set $\text{univ}$ (the set of all elements of type $\alpha$).

Set.iUnion_Icc_right theorem

(a : α) : ⋃ b, Icc a b = Ici a

Full source

@[simp]
theorem iUnion_Icc_right (a : α) : ⋃ b, Icc a b = Ici a := by
  simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]

Union of Closed Intervals with Fixed Left Endpoint Equals Right-Infinite Interval

Informal description

For any element $a$ in a preorder $\alpha$, the union of all closed intervals $[a, b]$ over all $b \in \alpha$ equals the left-closed right-infinite interval $[a, \infty)$.

Set.iUnion_Ioc_right theorem

(a : α) : ⋃ b, Ioc a b = Ioi a

Full source

@[simp]
theorem iUnion_Ioc_right (a : α) : ⋃ b, Ioc a b = Ioi a := by
  simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]

Union of Left-Open Right-Closed Intervals with Fixed Left Endpoint Equals Left-Open Right-Infinite Interval

Informal description

For any element $a$ in a preorder $\alpha$, the union of all left-open right-closed intervals $(a, b]$ over all $b \in \alpha$ equals the left-open right-infinite interval $(a, \infty)$.

Set.iUnion_Icc_left theorem

(b : α) : ⋃ a, Icc a b = Iic b

Full source

@[simp]
theorem iUnion_Icc_left (b : α) : ⋃ a, Icc a b = Iic b := by
  simp only [← Ici_inter_Iic, ← iUnion_inter, iUnion_Ici, univ_inter]

Union of Closed Intervals with Fixed Right Endpoint Equals Left-Infinite Interval

Informal description

For any element $b$ in a preorder $\alpha$, the union of all closed intervals $[a, b]$ over all $a \in \alpha$ equals the left-infinite right-closed interval $(-\infty, b]$.

Set.iUnion_Ico_left theorem

(b : α) : ⋃ a, Ico a b = Iio b

Full source

@[simp]
theorem iUnion_Ico_left (b : α) : ⋃ a, Ico a b = Iio b := by
  simp only [← Ici_inter_Iio, ← iUnion_inter, iUnion_Ici, univ_inter]

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

Informal description

For any element $b$ in a preorder $\alpha$, the union of all left-closed right-open intervals $[a, b)$ over all $a \in \alpha$ equals the left-infinite right-open interval $(-\infty, b)$.

Set.iUnion_Iio theorem

[NoMaxOrder α] : ⋃ a : α, Iio a = univ

Full source

@[simp]
theorem iUnion_Iio [NoMaxOrder α] : ⋃ a : α, Iio a = univ :=
  iUnion_eq_univ_iff.2 exists_gt

Union of left-infinite intervals covers the space in a no-max-order

Informal description

In a preorder $\alpha$ with no maximal element, the union of all left-infinite right-open intervals $(-\infty, a)$ for $a \in \alpha$ equals the universal set $\alpha$.

Set.iUnion_Ioi theorem

[NoMinOrder α] : ⋃ a : α, Ioi a = univ

Full source

@[simp]
theorem iUnion_Ioi [NoMinOrder α] : ⋃ a : α, Ioi a = univ :=
  iUnion_eq_univ_iff.2 exists_lt

Union of Right-Infinite Intervals Covers the Universe in No-Min-Order Preorders

Informal description

In a preorder $\alpha$ with no minimal element, the union of all left-open right-infinite intervals $\bigcup_{a \in \alpha} (a, \infty)$ is equal to the universal set $\alpha$.

Set.iUnion_Ico_right theorem

[NoMaxOrder α] (a : α) : ⋃ b, Ico a b = Ici a

Full source

@[simp]
theorem iUnion_Ico_right [NoMaxOrder α] (a : α) : ⋃ b, Ico a b = Ici a := by
  simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]

Union of Left-Closed Right-Open Intervals Equals Left-Closed Right-Infinite Interval in No-Max-Order Preorders

Informal description

For any element $a$ in a preorder $\alpha$ with no maximal element, the union of all left-closed right-open intervals $[a, b)$ over all $b \in \alpha$ equals the left-closed right-infinite interval $[a, \infty)$. In symbols: \[ \bigcup_{b \in \alpha} [a, b) = [a, \infty) \]

Set.iUnion_Ioo_right theorem

[NoMaxOrder α] (a : α) : ⋃ b, Ioo a b = Ioi a

Full source

@[simp]
theorem iUnion_Ioo_right [NoMaxOrder α] (a : α) : ⋃ b, Ioo a b = Ioi a := by
  simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]

Union of Open Right Intervals Equals Right-Infinite Interval in No-Max-Order Preorders

Informal description

For any element $a$ in a preorder $\alpha$ with no maximal element, the union of all open intervals $(a, b)$ over all $b \in \alpha$ equals the left-open right-infinite interval $(a, \infty)$. In symbols: \[ \bigcup_{b \in \alpha} (a, b) = (a, \infty) \]

Set.iUnion_Ioc_left theorem

[NoMinOrder α] (b : α) : ⋃ a, Ioc a b = Iic b

Full source

@[simp]
theorem iUnion_Ioc_left [NoMinOrder α] (b : α) : ⋃ a, Ioc a b = Iic b := by
  simp only [← Ioi_inter_Iic, ← iUnion_inter, iUnion_Ioi, univ_inter]

Union of Left-Open Right-Closed Intervals Equals Left-Infinite Right-Closed Interval in No-Min-Order Preorders

Informal description

For any element $b$ in a preorder $\alpha$ with no minimal element, the union of all left-open right-closed intervals $(a, b]$ over all $a \in \alpha$ equals the left-infinite right-closed interval $(-\infty, b]$. In symbols: \[ \bigcup_{a \in \alpha} (a, b] = (-\infty, b] \]

Set.iUnion_Ioo_left theorem

[NoMinOrder α] (b : α) : ⋃ a, Ioo a b = Iio b

Full source

@[simp]
theorem iUnion_Ioo_left [NoMinOrder α] (b : α) : ⋃ a, Ioo a b = Iio b := by
  simp only [← Ioi_inter_Iio, ← iUnion_inter, iUnion_Ioi, univ_inter]

Union of Open Left Intervals Equals Left-Infinite Interval in No-Min-Order Preorders

Informal description

For any element $b$ in a preorder $\alpha$ with no minimal element, the union of all open intervals $(a, b)$ over all $a \in \alpha$ equals the left-infinite right-open interval $(-\infty, b)$. In symbols: \[ \bigcup_{a \in \alpha} (a, b) = (-\infty, b) \]

Set.Ico_disjoint_Ico theorem

: Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Full source

@[simp]
theorem Ico_disjoint_Ico : DisjointDisjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ := by
  simp_rw [Set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, not_lt]

Disjointness Criterion for Half-Open Intervals: $\min(a₂, b₂) \leq \max(a₁, b₁)$

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a linear order, the half-open intervals $[a₁, a₂)$ and $[b₁, b₂)$ are disjoint if and only if the minimum of $a₂$ and $b₂$ is less than or equal to the maximum of $a₁$ and $b₁$. In symbols: \[ [a₁, a₂) \cap [b₁, b₂) = \emptyset \quad \Leftrightarrow \quad \min(a₂, b₂) \leq \max(a₁, b₁). \]

Set.Ioc_disjoint_Ioc theorem

: Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Full source

@[simp]
theorem Ioc_disjoint_Ioc : DisjointDisjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ := by
  have h : _ ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂) := Ico_disjoint_Ico
  simpa only [Ico_toDual] using h

Disjointness Criterion for Left-Open Right-Closed Intervals: $\min(a₂, b₂) \leq \max(a₁, b₁)$

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a linear order, the left-open right-closed intervals $(a₁, a₂]$ and $(b₁, b₂]$ are disjoint if and only if the minimum of $a₂$ and $b₂$ is less than or equal to the maximum of $a₁$ and $b₁$. In symbols: \[ (a₁, a₂] \cap (b₁, b₂] = \emptyset \quad \Leftrightarrow \quad \min(a₂, b₂) \leq \max(a₁, b₁). \]

Set.Ioo_disjoint_Ioo theorem

[DenselyOrdered α] : Disjoint (Set.Ioo a₁ a₂) (Set.Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Full source

@[simp]
theorem Ioo_disjoint_Ioo [DenselyOrdered α] :
    DisjointDisjoint (Set.Ioo a₁ a₂) (Set.Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ := by
  simp_rw [Set.disjoint_iff_inter_eq_empty, Ioo_inter_Ioo, Ioo_eq_empty_iff, not_lt]

Disjointness Criterion for Open Intervals in Densely Ordered Sets

Informal description

In a densely ordered set $\alpha$, two open intervals $(a₁, a₂)$ and $(b₁, b₂)$ are disjoint if and only if the minimum of their right endpoints is less than or equal to the maximum of their left endpoints, i.e., \[ (a₁, a₂) \cap (b₁, b₂) = \emptyset \quad \Leftrightarrow \quad \min(a₂, b₂) \leq \max(a₁, b₁). \]

Set.iUnion_Ico_eq_Iio_self_iff theorem

{f : ι → α} {a : α} : ⋃ i, Ico (f i) a = Iio a ↔ ∀ x < a, ∃ i, f i ≤ x

Full source

@[simp]
theorem iUnion_Ico_eq_Iio_self_iff {f : ι → α} {a : α} :
    ⋃ i, Ico (f i) a⋃ i, Ico (f i) a = Iio a ↔ ∀ x < a, ∃ i, f i ≤ x := by
  simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

Union of Left-Closed Right-Open Intervals Equals Left-Infinite Right-Open Interval Criterion

Informal description

Let $\alpha$ be a type with a preorder, and let $f : \iota \to \alpha$ be a family of elements in $\alpha$ indexed by $\iota$. For any $a \in \alpha$, the union of the left-closed right-open intervals $[f(i), a)$ over all $i \in \iota$ equals the left-infinite right-open interval $(-\infty, a)$ if and only if for every $x < a$, there exists an index $i \in \iota$ such that $f(i) \leq x$.

Set.iUnion_Ioc_eq_Ioi_self_iff theorem

{f : ι → α} {a : α} : ⋃ i, Ioc a (f i) = Ioi a ↔ ∀ x, a < x → ∃ i, x ≤ f i

Full source

@[simp]
theorem iUnion_Ioc_eq_Ioi_self_iff {f : ι → α} {a : α} :
    ⋃ i, Ioc a (f i)⋃ i, Ioc a (f i) = Ioi a ↔ ∀ x, a < x → ∃ i, x ≤ f i := by
  simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]

Union of Right-Closed Intervals Equals Right-Infinite Interval iff Bounded Above

Informal description

For a family of functions $ f : \iota \to \alpha $ and an element $ a \in \alpha $, the union of left-open right-closed intervals $ \bigcup_i (a, f(i)] $ equals the left-open right-infinite interval $ (a, \infty) $ if and only if for every $ x > a $, there exists an index $ i $ such that $ x \leq f(i) $.

Set.biUnion_Ico_eq_Iio_self_iff theorem

 {p : ι → Prop} {f : ∀ i, p i → α} {a : α} : ⋃ (i) (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ x < a, ∃ i hi, f i hi ≤ x

Full source

@[simp]
theorem biUnion_Ico_eq_Iio_self_iff {p : ι → Prop} {f : ∀ i, p i → α} {a : α} :
    ⋃ (i) (hi : p i), Ico (f i hi) a⋃ (i) (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ x < a, ∃ i hi, f i hi ≤ x := by
  simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

Union of Left-Closed Right-Open Intervals Equals Left-Infinite Right-Open Interval Criterion

Informal description

Let $\alpha$ be a preorder, $p : \iota \to \text{Prop}$ a predicate on an index type $\iota$, $f : \forall i, p(i) \to \alpha$ a family of elements in $\alpha$ indexed by $\iota$ and satisfying $p$, and $a \in \alpha$. Then the union of left-closed right-open intervals $\bigcup_{i, h_i : p(i)} [f(i, h_i), a)$ equals the left-infinite right-open interval $(-\infty, a)$ if and only if for every $x < a$, there exists an index $i$ with $p(i)$ and a proof $h_i$ such that $f(i, h_i) \leq x$.

Set.biUnion_Ioc_eq_Ioi_self_iff theorem

 {p : ι → Prop} {f : ∀ i, p i → α} {a : α} : ⋃ (i) (hi : p i), Ioc a (f i hi) = Ioi a ↔ ∀ x, a < x → ∃ i hi, x ≤ f i hi

Full source

@[simp]
theorem biUnion_Ioc_eq_Ioi_self_iff {p : ι → Prop} {f : ∀ i, p i → α} {a : α} :
    ⋃ (i) (hi : p i), Ioc a (f i hi)⋃ (i) (hi : p i), Ioc a (f i hi) = Ioi a ↔ ∀ x, a < x → ∃ i hi, x ≤ f i hi := by
  simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]

Union of Right-Closed Intervals Equals Right-Infinite Interval Characterization

Informal description

For a predicate $p$ on an index type $\iota$, a family of functions $f$ from $\{i \mid p i\}$ to a preorder $\alpha$, and an element $a \in \alpha$, the union of left-open right-closed intervals $\bigcup_{i, p i} (a, f i]$ equals the left-open right-infinite interval $(a, \infty)$ if and only if for every $x > a$, there exists an index $i$ with $p i$ such that $x \leq f i$.

IsGLB.biUnion_Ioi_eq theorem

(h : IsGLB s a) : ⋃ x ∈ s, Ioi x = Ioi a

Full source

theorem IsGLB.biUnion_Ioi_eq (h : IsGLB s a) : ⋃ x ∈ s, Ioi x = Ioi a := by
  refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
  · exact Ioi_subset_Ioi (h.1 hx)
  · rcases h.exists_between hx with ⟨y, hys, _, hyx⟩
    exact mem_biUnion hys hyx

Union of Right-Infinite Intervals Equals Right-Infinite Interval at Greatest Lower Bound

Informal description

Let $s$ be a subset of a preorder $\alpha$ and $a$ be an element of $\alpha$. If $a$ is the greatest lower bound of $s$, then the union of all left-open right-infinite intervals $(x, \infty)$ for $x \in s$ is equal to the left-open right-infinite interval $(a, \infty)$. In other words, $\bigcup_{x \in s} (x, \infty) = (a, \infty)$.

IsGLB.iUnion_Ioi_eq theorem

(h : IsGLB (range f) a) : ⋃ x, Ioi (f x) = Ioi a

Full source

theorem IsGLB.iUnion_Ioi_eq (h : IsGLB (range f) a) : ⋃ x, Ioi (f x) = Ioi a :=
  biUnion_range.symm.trans h.biUnion_Ioi_eq

Union of Right-Infinite Intervals at Function Values Equals Interval at Greatest Lower Bound

Informal description

Let $f$ be a function from some index type to a preorder $\alpha$, and let $a \in \alpha$ be the greatest lower bound of the range of $f$. Then the union of all left-open right-infinite intervals $(f(x), \infty)$ for $x$ in the index type equals the left-open right-infinite interval $(a, \infty)$. In other words, $\bigcup_x (f(x), \infty) = (a, \infty)$.

IsLUB.biUnion_Iio_eq theorem

(h : IsLUB s a) : ⋃ x ∈ s, Iio x = Iio a

Full source

theorem IsLUB.biUnion_Iio_eq (h : IsLUB s a) : ⋃ x ∈ s, Iio x = Iio a :=
  h.dual.biUnion_Ioi_eq

Union of Left-Infinite Intervals Equals Left-Infinite Interval at Least Upper Bound

Informal description

Let $s$ be a subset of a preorder $\alpha$ and $a$ be an element of $\alpha$. If $a$ is the least upper bound of $s$, then the union of all left-infinite right-open intervals $(-\infty, x)$ for $x \in s$ is equal to the left-infinite right-open interval $(-\infty, a)$. In other words, $\bigcup_{x \in s} (-\infty, x) = (-\infty, a)$.

IsGLB.biUnion_Ici_eq_Ioi theorem

(a_glb : IsGLB s a) (a_not_mem : a ∉ s) : ⋃ x ∈ s, Ici x = Ioi a

Full source

theorem IsGLB.biUnion_Ici_eq_Ioi (a_glb : IsGLB s a) (a_not_mem : a ∉ s) :
    ⋃ x ∈ s, Ici x = Ioi a := by
  refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
  · exact Ici_subset_Ioi.mpr (lt_of_le_of_ne (a_glb.1 hx) fun h => (h ▸ a_not_mem) hx)
  · rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩
    rw [mem_iUnion₂]
    exact ⟨y, hys, hyx.le⟩

Union of Left-Closed Right-Infinite Intervals Equals Left-Open Right-Infinite Interval at Greatest Lower Bound

Informal description

Let $s$ be a set in a preorder $\alpha$, and let $a$ be the greatest lower bound of $s$. If $a$ does not belong to $s$, then the union of the left-closed right-infinite intervals $[x, \infty)$ for all $x \in s$ is equal to the left-open right-infinite interval $(a, \infty)$.

IsGLB.biUnion_Ici_eq_Ici theorem

(a_glb : IsGLB s a) (a_mem : a ∈ s) : ⋃ x ∈ s, Ici x = Ici a

Full source

theorem IsGLB.biUnion_Ici_eq_Ici (a_glb : IsGLB s a) (a_mem : a ∈ s) :
    ⋃ x ∈ s, Ici x = Ici a := by
  refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
  · exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)
  · exact mem_iUnion₂.mpr ⟨a, a_mem, hx⟩

Union of Left-Closed Right-Infinite Intervals Equals $[a, \infty)$ When $a$ is the Greatest Lower Bound and $a \in s$

Informal description

Let $s$ be a set in a preorder $\alpha$, and let $a$ be the greatest lower bound of $s$ (i.e., $\text{IsGLB}(s, a)$). If $a$ is an element of $s$, then the union of all left-closed right-infinite intervals $[x, \infty)$ for $x \in s$ is equal to the interval $[a, \infty)$. In symbols: \[ \bigcup_{x \in s} [x, \infty) = [a, \infty). \]

IsLUB.biUnion_Iic_eq_Iio theorem

(a_lub : IsLUB s a) (a_not_mem : a ∉ s) : ⋃ x ∈ s, Iic x = Iio a

Full source

theorem IsLUB.biUnion_Iic_eq_Iio (a_lub : IsLUB s a) (a_not_mem : a ∉ s) :
    ⋃ x ∈ s, Iic x = Iio a :=
  a_lub.dual.biUnion_Ici_eq_Ioi a_not_mem

Union of Right-Closed Left-Infinite Intervals Equals Right-Open Left-Infinite Interval at Least Upper Bound

Informal description

Let $s$ be a set in a preorder $\alpha$, and let $a$ be the least upper bound of $s$. If $a$ does not belong to $s$, then the union of the left-infinite right-closed intervals $(-\infty, x]$ for all $x \in s$ is equal to the left-infinite right-open interval $(-\infty, a)$.

IsLUB.biUnion_Iic_eq_Iic theorem

(a_lub : IsLUB s a) (a_mem : a ∈ s) : ⋃ x ∈ s, Iic x = Iic a

Full source

theorem IsLUB.biUnion_Iic_eq_Iic (a_lub : IsLUB s a) (a_mem : a ∈ s) : ⋃ x ∈ s, Iic x = Iic a :=
  a_lub.dual.biUnion_Ici_eq_Ici a_mem

Union of Left-Infinite Right-Closed Intervals Equals $(-\infty, a]$ When $a$ is the Least Upper Bound and $a \in s$

Informal description

Let $s$ be a set in a preorder $\alpha$, and let $a$ be the least upper bound of $s$ (i.e., $\text{IsLUB}(s, a)$). If $a$ is an element of $s$, then the union of all left-infinite right-closed intervals $(-\infty, x]$ for $x \in s$ is equal to the interval $(-\infty, a]$. In symbols: \[ \bigcup_{x \in s} (-\infty, x] = (-\infty, a]. \]

iUnion_Ici_eq_Ioi_iInf theorem

 {R : Type*} [CompleteLinearOrder R] {f : ι → R} (no_least_elem : ⨅ i, f i ∉ range f) :
  ⋃ i : ι, Ici (f i) = Ioi (⨅ i, f i)

Full source

theorem iUnion_Ici_eq_Ioi_iInf {R : Type*} [CompleteLinearOrder R] {f : ι → R}
    (no_least_elem : ⨅ i, f i⨅ i, f i ∉ range f) : ⋃ i : ι, Ici (f i) = Ioi (⨅ i, f i) := by
  simp only [← IsGLB.biUnion_Ici_eq_Ioi (@isGLB_iInf _ _ _ f) no_least_elem, mem_range,
    iUnion_exists, iUnion_iUnion_eq']

Union of Closed Rays Equals Open Ray at Infimum When Infimum Not in Range

Informal description

Let $R$ be a complete linear order and $f : \iota \to R$ be a function. If the infimum of the range of $f$ does not belong to the range of $f$, then the union of the left-closed right-infinite intervals $[f(i), \infty)$ for all $i \in \iota$ is equal to the left-open right-infinite interval $(\inf f, \infty)$.

iUnion_Iic_eq_Iio_iSup theorem

 {R : Type*} [CompleteLinearOrder R] {f : ι → R} (no_greatest_elem : (⨆ i, f i) ∉ range f) :
  ⋃ i : ι, Iic (f i) = Iio (⨆ i, f i)

Full source

theorem iUnion_Iic_eq_Iio_iSup {R : Type*} [CompleteLinearOrder R] {f : ι → R}
    (no_greatest_elem : (⨆ i, f i) ∉ range f) : ⋃ i : ι, Iic (f i) = Iio (⨆ i, f i) :=
  @iUnion_Ici_eq_Ioi_iInf ι (OrderDual R) _ f no_greatest_elem

Union of Left-Closed Intervals Equals Left-Open Interval at Supremum When Supremum Not in Range

Informal description

Let $R$ be a complete linear order and $f : \iota \to R$ be a function. If the supremum of the range of $f$ does not belong to the range of $f$, then the union of the left-infinite right-closed intervals $(-\infty, f(i)]$ for all $i \in \iota$ is equal to the left-infinite right-open interval $(-\infty, \sup f)$. In symbols: \[ \bigcup_{i \in \iota} (-\infty, f(i)] = (-\infty, \sup f). \]

iUnion_Ici_eq_Ici_iInf theorem

 {R : Type*} [CompleteLinearOrder R] {f : ι → R} (has_least_elem : (⨅ i, f i) ∈ range f) :
  ⋃ i : ι, Ici (f i) = Ici (⨅ i, f i)

Full source

theorem iUnion_Ici_eq_Ici_iInf {R : Type*} [CompleteLinearOrder R] {f : ι → R}
    (has_least_elem : (⨅ i, f i) ∈ range f) : ⋃ i : ι, Ici (f i) = Ici (⨅ i, f i) := by
  simp only [← IsGLB.biUnion_Ici_eq_Ici (@isGLB_iInf _ _ _ f) has_least_elem, mem_range,
    iUnion_exists, iUnion_iUnion_eq']

Union of Closed Rays Equals Closed Ray at Infimum When Infimum is Achieved

Informal description

Let $R$ be a complete linear order and $f : \iota \to R$ be a function. If the infimum of the range of $f$ belongs to the range of $f$, then the union of the left-closed right-infinite intervals $[f(i), \infty)$ for all $i \in \iota$ is equal to the left-closed right-infinite interval $[\inf f, \infty)$. In symbols: \[ \bigcup_{i \in \iota} [f(i), \infty) = [\inf f, \infty). \]

iUnion_Iic_eq_Iic_iSup theorem

 {R : Type*} [CompleteLinearOrder R] {f : ι → R} (has_greatest_elem : (⨆ i, f i) ∈ range f) :
  ⋃ i : ι, Iic (f i) = Iic (⨆ i, f i)

Full source

theorem iUnion_Iic_eq_Iic_iSup {R : Type*} [CompleteLinearOrder R] {f : ι → R}
    (has_greatest_elem : (⨆ i, f i) ∈ range f) : ⋃ i : ι, Iic (f i) = Iic (⨆ i, f i) :=
  @iUnion_Ici_eq_Ici_iInf ι (OrderDual R) _ f has_greatest_elem

Union of Left-Closed Intervals Equals Left-Closed Interval at Supremum When Supremum is Achieved

Informal description

Let $R$ be a complete linear order and $f : \iota \to R$ be a function. If the supremum of the range of $f$ belongs to the range of $f$, then the union of the left-infinite right-closed intervals $(-\infty, f(i)]$ for all $i \in \iota$ is equal to the left-infinite right-closed interval $(-\infty, \sup f]$. In symbols: \[ \bigcup_{i \in \iota} (-\infty, f(i)] = (-\infty, \sup f]. \]

iUnion_Iio_eq_univ_iff theorem

: ⋃ i, Iio (f i) = univ ↔ (¬BddAbove (range f))

Full source

theorem iUnion_Iio_eq_univ_iff : ⋃ i, Iio (f i)⋃ i, Iio (f i) = univ ↔ (¬ BddAbove (range f)) := by
  simp [not_bddAbove_iff, Set.eq_univ_iff_forall]

Union of Left-Infinite Intervals Equals Universal Set iff Range is Unbounded Above

Informal description

For a family of functions $f : \iota \to R$ where $R$ is a complete linear order, the union of all left-infinite right-open intervals $(-\infty, f(i))$ equals the universal set if and only if the range of $f$ is not bounded above. In other words: \[ \bigcup_{i \in \iota} (-\infty, f(i)) = \text{univ} \iff \text{the range of } f \text{ is not bounded above.} \]

iUnion_Iic_of_not_bddAbove_range theorem

(hf : ¬BddAbove (range f)) : ⋃ i, Iic (f i) = univ

Full source

theorem iUnion_Iic_of_not_bddAbove_range (hf : ¬ BddAbove (range f)) : ⋃ i, Iic (f i) = univ := by
  refine  Set.eq_univ_of_subset ?_ (iUnion_Iio_eq_univ_iff.mpr hf)
  gcongr
  exact Iio_subset_Iic_self

Union of Left-Infinite Closed Intervals Equals Universal Set for Unbounded Above Functions

Informal description

For a function $f : \iota \to R$ where $R$ is a complete linear order, if the range of $f$ is not bounded above, then the union of all left-infinite right-closed intervals $(-\infty, f(i)]$ equals the universal set. In other words: \[ \text{If } f \text{ is not bounded above, then } \bigcup_{i \in \iota} (-\infty, f(i)] = \text{univ}. \]

iInter_Iic_eq_empty_iff theorem

: ⋂ i, Iic (f i) = ∅ ↔ ¬BddBelow (range f)

Full source

theorem iInter_Iic_eq_empty_iff : ⋂ i, Iic (f i)⋂ i, Iic (f i) = ∅ ↔ ¬ BddBelow (range f) := by
  simp [not_bddBelow_iff, Set.eq_empty_iff_forall_not_mem]

Empty Intersection of Left-Infinite Right-Closed Intervals iff Unbounded Below

Informal description

The intersection of all left-infinite right-closed intervals $(-\infty, f(i)]$ over all indices $i$ is empty if and only if the range of $f$ is not bounded below.

iInter_Iio_of_not_bddBelow_range theorem

(hf : ¬BddBelow (range f)) : ⋂ i, Iio (f i) = ∅

Full source

theorem iInter_Iio_of_not_bddBelow_range (hf : ¬ BddBelow (range f)) : ⋂ i, Iio (f i) = ∅ := by
  refine eq_empty_of_subset_empty ?_
  rw [← iInter_Iic_eq_empty_iff.mpr hf]
  gcongr
  exact Iio_subset_Iic_self

Empty Intersection of Left-Infinite Right-Open Intervals for Unbounded Below Functions

Informal description

For a function $f$ whose range is not bounded below, the intersection of all left-infinite right-open intervals $(-\infty, f(i))$ over all indices $i$ is empty, i.e., $\bigcap_i (-\infty, f(i)) = \emptyset$.