# Extra lemmas about intervals #

This file contains lemmas about intervals that cannot be included into `Order.Interval.Set.Basic` because this would create an `import` cycle. Namely, lemmas in this file can use definitions from `Data.Set.Lattice`, including `Disjoint`.

We consider various intersections and unions of half infinite intervals.

source
@[simp]
theorem Set.Iic_disjoint_Ioi {α : Type v} [Preorder α] {a b : α} (h : a ≤ b) :
Disjoint (Iic a) (Ioi b)
source
@[simp]
theorem Set.Iio_disjoint_Ici {α : Type v} [Preorder α] {a b : α} (h : a ≤ b) :
Disjoint (Iio a) (Ici b)
source
@[simp]
theorem Set.Iic_disjoint_Ioc {α : Type v} [Preorder α] {a b c : α} (h : a ≤ b) :
Disjoint (Iic a) (Ioc b c)
source
@[simp]
theorem Set.Ioc_disjoint_Ioc_of_le {α : Type v} [Preorder α] {a b c d : α} (h : b ≤ c) :
Disjoint (Ioc a b) (Ioc c d)
source
@[simp]
theorem Set.Ico_disjoint_Ico_same {α : Type v} [Preorder α] {a b c : α} :
Disjoint (Ico a b) (Ico b c)
source
@[simp]
theorem Set.Ici_disjoint_Iic {α : Type v} [Preorder α] {a b : α} :
Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b
source
@[simp]
theorem Set.Iic_disjoint_Ici {α : Type v} [Preorder α] {a b : α} :
Disjoint (Iic a) (Ici b) ↔ ¬b ≤ a
source
@[simp]
theorem Set.Ioc_disjoint_Ioi {α : Type v} [Preorder α] {a b c : α} (h : b ≤ c) :
Disjoint (Ioc a b) (Ioi c)
source
theorem Set.Ioc_disjoint_Ioi_same {α : Type v} [Preorder α] {a b : α} :
Disjoint (Ioc a b) (Ioi b)
source
theorem Set.Ioi_disjoint_Iio_of_not_lt {α : Type v} [Preorder α] {a b : α} (h : ¬a < b) :
Disjoint (Ioi a) (Iio b)
source
theorem Set.Ioi_disjoint_Iio_of_le {α : Type v} [Preorder α] {a b : α} (h : a ≤ b) :
Disjoint (Ioi b) (Iio a)
source
@[simp]
theorem Set.Ioi_disjoint_Iio_same {α : Type v} [Preorder α] {a : α} :
Disjoint (Ioi a) (Iio a)
source
@[simp]
theorem Set.Ioi_disjoint_Iio_iff {α : Type v} [Preorder α] {a b : α} [DenselyOrdered α] :
Disjoint (Ioi a) (Iio b) ↔ ¬a < b
source
theorem Set.Iio_disjoint_Ioi_of_not_lt {α : Type v} [Preorder α] {a b : α} (h : ¬a < b) :
Disjoint (Iio b) (Ioi a)
source
theorem Set.Iio_disjoint_Ioi_of_le {α : Type v} [Preorder α] {a b : α} (h : a ≤ b) :
Disjoint (Iio a) (Ioi b)
source
@[simp]
theorem Set.Iio_disjoint_Ioi_same {α : Type v} [Preorder α] {a : α} :
Disjoint (Iio a) (Ioi a)
source
@[simp]
theorem Set.Iio_disjoint_Ioi_iff {α : Type v} [Preorder α] {a b : α} [DenselyOrdered α] :
Disjoint (Iio a) (Ioi b) ↔ ¬b < a
source
@[simp]
theorem Set.iUnion_Iic {α : Type v} [Preorder α] :
⋃ (a : α), Iic a = univ
source
@[simp]
theorem Set.iUnion_Ici {α : Type v} [Preorder α] :
⋃ (a : α), Ici a = univ
source
@[simp]
theorem Set.iUnion_Icc_right {α : Type v} [Preorder α] (a : α) :
⋃ (b : α), Icc a b = Ici a
source
@[simp]
theorem Set.iUnion_Ioc_right {α : Type v} [Preorder α] (a : α) :
⋃ (b : α), Ioc a b = Ioi a
source
@[simp]
theorem Set.iUnion_Icc_left {α : Type v} [Preorder α] (b : α) :
⋃ (a : α), Icc a b = Iic b
source
@[simp]
theorem Set.iUnion_Ico_left {α : Type v} [Preorder α] (b : α) :
⋃ (a : α), Ico a b = Iio b
source
@[simp]
theorem Set.iUnion_Iio {α : Type v} [Preorder α] [NoMaxOrder α] :
⋃ (a : α), Iio a = univ
source
@[simp]
theorem Set.iUnion_Ioi {α : Type v} [Preorder α] [NoMinOrder α] :
⋃ (a : α), Ioi a = univ
source
@[simp]
theorem Set.iUnion_Ico_right {α : Type v} [Preorder α] [NoMaxOrder α] (a : α) :
⋃ (b : α), Ico a b = Ici a
source
@[simp]
theorem Set.iUnion_Ioo_right {α : Type v} [Preorder α] [NoMaxOrder α] (a : α) :
⋃ (b : α), Ioo a b = Ioi a
source
@[simp]
theorem Set.iUnion_Ioc_left {α : Type v} [Preorder α] [NoMinOrder α] (b : α) :
⋃ (a : α), Ioc a b = Iic b
source
@[simp]
theorem Set.iUnion_Ioo_left {α : Type v} [Preorder α] [NoMinOrder α] (b : α) :
⋃ (a : α), Ioo a b = Iio b
source
@[simp]
theorem Set.Ico_disjoint_Ico {α : Type v} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} :
Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
source
@[simp]
theorem Set.Ioc_disjoint_Ioc {α : Type v} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} :
Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
source
@[simp]
theorem Set.Ioo_disjoint_Ioo {α : Type v} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} [DenselyOrdered α] :
Disjoint (Ioo a₁ a₂) (Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
source
theorem Set.eq_of_Ico_disjoint {α : Type v} [LinearOrder α] {x₁ x₂ y₁ y₂ : α} (h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)) (hx : x₁ < x₂) (h2 : x₂ ∈ Ico y₁ y₂) :
y₁ = x₂

If two half-open intervals are disjoint and the endpoint of one lies in the other, then it must be equal to the endpoint of the other.

source
@[simp]
theorem Set.iUnion_Ico_eq_Iio_self_iff {ι : Sort u} {α : Type v} [LinearOrder α] {f : ι → α} {a : α} :
⋃ (i : ι), Ico (f i) a = Iio a ↔ ∀ x < a, ∃ (i : ι), f i ≤ x
source
@[simp]
theorem Set.iUnion_Ioc_eq_Ioi_self_iff {ι : Sort u} {α : Type v} [LinearOrder α] {f : ι → α} {a : α} :
⋃ (i : ι), Ioc a (f i) = Ioi a ↔ ∀ (x : α), a < x → ∃ (i : ι), x ≤ f i
source
@[simp]
theorem Set.biUnion_Ico_eq_Iio_self_iff {ι : Sort u} {α : Type v} [LinearOrder α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} :
⋃ (i : ι), ⋃ (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ x < a, ∃ (i : ι) (hi : p i), f i hi ≤ x
source
@[simp]
theorem Set.biUnion_Ioc_eq_Ioi_self_iff {ι : Sort u} {α : Type v} [LinearOrder α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} :
⋃ (i : ι), ⋃ (hi : p i), Ioc a (f i hi) = Ioi a ↔ ∀ (x : α), a < x → ∃ (i : ι) (hi : p i), x ≤ f i hi
source
theorem IsGLB.biUnion_Ioi_eq {α : Type v} [LinearOrder α] {s : Set α} {a : α} (h : IsGLB s a) :
⋃ x ∈ s, Set.Ioi x = Set.Ioi a
source
theorem IsGLB.iUnion_Ioi_eq {ι : Sort u} {α : Type v} [LinearOrder α] {a : α} {f : ι → α} (h : IsGLB (Set.range f) a) :
⋃ (x : ι), Set.Ioi (f x) = Set.Ioi a
source
theorem IsLUB.biUnion_Iio_eq {α : Type v} [LinearOrder α] {s : Set α} {a : α} (h : IsLUB s a) :
⋃ x ∈ s, Set.Iio x = Set.Iio a
source
theorem IsLUB.iUnion_Iio_eq {ι : Sort u} {α : Type v} [LinearOrder α] {a : α} {f : ι → α} (h : IsLUB (Set.range f) a) :
⋃ (x : ι), Set.Iio (f x) = Set.Iio a
source
theorem IsGLB.biUnion_Ici_eq_Ioi {α : Type v} [LinearOrder α] {s : Set α} {a : α} (a_glb : IsGLB s a) (a_notMem : a ∉ s) :
⋃ x ∈ s, Set.Ici x = Set.Ioi a
source
theorem IsGLB.biUnion_Ici_eq_Ici {α : Type v} [LinearOrder α] {s : Set α} {a : α} (a_glb : IsGLB s a) (a_mem : a ∈ s) :
⋃ x ∈ s, Set.Ici x = Set.Ici a
source
theorem IsLUB.biUnion_Iic_eq_Iio {α : Type v} [LinearOrder α] {s : Set α} {a : α} (a_lub : IsLUB s a) (a_notMem : a ∉ s) :
⋃ x ∈ s, Set.Iic x = Set.Iio a
source
theorem IsLUB.biUnion_Iic_eq_Iic {α : Type v} [LinearOrder α] {s : Set α} {a : α} (a_lub : IsLUB s a) (a_mem : a ∈ s) :
⋃ x ∈ s, Set.Iic x = Set.Iic a
source
theorem iUnion_Ici_eq_Ioi_iInf {ι : Sort u} {R : Type u_1} [CompleteLinearOrder R] {f : ι → R} (no_least_elem : ⨅ (i : ι), f i ∉ Set.range f) :
⋃ (i : ι), Set.Ici (f i) = Set.Ioi (⨅ (i : ι), f i)
source
theorem iUnion_Iic_eq_Iio_iSup {ι : Sort u} {R : Type u_1} [CompleteLinearOrder R] {f : ι → R} (no_greatest_elem : ⨆ (i : ι), f i ∉ Set.range f) :
⋃ (i : ι), Set.Iic (f i) = Set.Iio (⨆ (i : ι), f i)
source
theorem iUnion_Ici_eq_Ici_iInf {ι : Sort u} {R : Type u_1} [CompleteLinearOrder R] {f : ι → R} (has_least_elem : ⨅ (i : ι), f i ∈ Set.range f) :
⋃ (i : ι), Set.Ici (f i) = Set.Ici (⨅ (i : ι), f i)
source
theorem iUnion_Iic_eq_Iic_iSup {ι : Sort u} {R : Type u_1} [CompleteLinearOrder R] {f : ι → R} (has_greatest_elem : ⨆ (i : ι), f i ∈ Set.range f) :
⋃ (i : ι), Set.Iic (f i) = Set.Iic (⨆ (i : ι), f i)
source
theorem iUnion_Iio_eq_univ_iff {ι : Sort u} {α : Type v} [LinearOrder α] {f : ι → α} :
⋃ (i : ι), Set.Iio (f i) = Set.univ ↔ ¬BddAbove (Set.range f)
source
theorem iUnion_Iic_of_not_bddAbove_range {ι : Sort u} {α : Type v} [LinearOrder α] {f : ι → α} (hf : ¬BddAbove (Set.range f)) :
⋃ (i : ι), Set.Iic (f i) = Set.univ
source
theorem iInter_Iic_eq_empty_iff {ι : Sort u} {α : Type v} [LinearOrder α] {f : ι → α} :
⋂ (i : ι), Set.Iic (f i) = ∅ ↔ ¬BddBelow (Set.range f)
source
theorem iInter_Iio_of_not_bddBelow_range {ι : Sort u} {α : Type v} [LinearOrder α] {f : ι → α} (hf : ¬BddBelow (Set.range f)) :
⋂ (i : ι), Set.Iio (f i) = ∅