Extra lemmas about intervals

This file contains lemmas about intervals that cannot be included into Mathlib/Order/Interval/Set/Basic.lean 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.

@[simp]

theorem Set.Iic_disjoint_Ioi {α : Type v} [Preorder α] {a b : α} (h : a ≤ b) : Disjoint (Iic a) (Ioi b)

@[simp]

theorem Set.Iio_disjoint_Ici {α : Type v} [Preorder α] {a b : α} (h : a ≤ b) : Disjoint (Iio a) (Ici b)

@[simp]

theorem Set.Iic_disjoint_Ioc {α : Type v} [Preorder α] {a b c : α} (h : a ≤ b) : Disjoint (Iic a) (Ioc b c)

@[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)

@[simp]

theorem Set.Ico_disjoint_Ico_same {α : Type v} [Preorder α] {a b c : α} : Disjoint (Ico a b) (Ico b c)

@[simp]

theorem Set.Ici_disjoint_Iic {α : Type v} [Preorder α] {a b : α} : Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b

@[simp]

theorem Set.Iic_disjoint_Ici {α : Type v} [Preorder α] {a b : α} : Disjoint (Iic a) (Ici b) ↔ ¬b ≤ a

@[simp]

theorem Set.Ioc_disjoint_Ioi {α : Type v} [Preorder α] {a b c : α} (h : b ≤ c) : Disjoint (Ioc a b) (Ioi c)

theorem Set.Ioc_disjoint_Ioi_same {α : Type v} [Preorder α] {a b : α} : Disjoint (Ioc a b) (Ioi b)

theorem Set.Ioi_disjoint_Iio_of_not_lt {α : Type v} [Preorder α] {a b : α} (h : ¬a < b) : Disjoint (Ioi a) (Iio b)

theorem Set.Ioi_disjoint_Iio_of_le {α : Type v} [Preorder α] {a b : α} (h : a ≤ b) : Disjoint (Ioi b) (Iio a)

@[simp]

theorem Set.Ioi_disjoint_Iio_same {α : Type v} [Preorder α] {a : α} : Disjoint (Ioi a) (Iio a)

@[simp]

theorem Set.Ioi_disjoint_Iio_iff {α : Type v} [Preorder α] {a b : α} [DenselyOrdered α] : Disjoint (Ioi a) (Iio b) ↔ ¬a < b

theorem Set.Iio_disjoint_Ioi_of_not_lt {α : Type v} [Preorder α] {a b : α} (h : ¬a < b) : Disjoint (Iio b) (Ioi a)

theorem Set.Iio_disjoint_Ioi_of_le {α : Type v} [Preorder α] {a b : α} (h : a ≤ b) : Disjoint (Iio a) (Ioi b)

@[simp]

theorem Set.Iio_disjoint_Ioi_same {α : Type v} [Preorder α] {a : α} : Disjoint (Iio a) (Ioi a)

@[simp]

theorem Set.Iio_disjoint_Ioi_iff {α : Type v} [Preorder α] {a b : α} [DenselyOrdered α] : Disjoint (Iio a) (Ioi b) ↔ ¬b < a

@[simp]

theorem Set.iUnion_Iic {α : Type v} [Preorder α] : ⋃ (a : α), Iic a = univ

@[simp]

theorem Set.iUnion_Ici {α : Type v} [Preorder α] : ⋃ (a : α), Ici a = univ

@[simp]

theorem Set.iUnion_Icc_right {α : Type v} [Preorder α] (a : α) : ⋃ (b : α), Icc a b = Ici a

@[simp]

theorem Set.iUnion_Ioc_right {α : Type v} [Preorder α] (a : α) : ⋃ (b : α), Ioc a b = Ioi a

@[simp]

theorem Set.iUnion_Icc_left {α : Type v} [Preorder α] (b : α) : ⋃ (a : α), Icc a b = Iic b

@[simp]

theorem Set.iUnion_Ico_left {α : Type v} [Preorder α] (b : α) : ⋃ (a : α), Ico a b = Iio b

@[simp]

theorem Set.iUnion_Iio {α : Type v} [Preorder α] [NoMaxOrder α] : ⋃ (a : α), Iio a = univ

@[simp]

theorem Set.iUnion_Ioi {α : Type v} [Preorder α] [NoMinOrder α] : ⋃ (a : α), Ioi a = univ

@[simp]

theorem Set.iUnion_Ico_right {α : Type v} [Preorder α] [NoMaxOrder α] (a : α) : ⋃ (b : α), Ico a b = Ici a

@[simp]

theorem Set.iUnion_Ioo_right {α : Type v} [Preorder α] [NoMaxOrder α] (a : α) : ⋃ (b : α), Ioo a b = Ioi a

@[simp]

theorem Set.iUnion_Ioc_left {α : Type v} [Preorder α] [NoMinOrder α] (b : α) : ⋃ (a : α), Ioc a b = Iic b

@[simp]

theorem Set.iUnion_Ioo_left {α : Type v} [Preorder α] [NoMinOrder α] (b : α) : ⋃ (a : α), Ioo a b = Iio b

@[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₁

@[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₁

@[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₁

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.

@[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

@[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

@[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

@[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

theorem IsGLB.biUnion_Ioi_eq {α : Type v} [LinearOrder α] {s : Set α} {a : α} (h : IsGLB s a) : ⋃ x ∈ s, Set.Ioi x = Set.Ioi a

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

theorem IsLUB.biUnion_Iio_eq {α : Type v} [LinearOrder α] {s : Set α} {a : α} (h : IsLUB s a) : ⋃ x ∈ s, Set.Iio x = Set.Iio a

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

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

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

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

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

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)

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)

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)

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)

theorem iUnion_Iio_eq_univ_iff {ι : Sort u} {α : Type v} [LinearOrder α] {f : ι → α} : ⋃ (i : ι), Set.Iio (f i) = Set.univ ↔ ¬BddAbove (Set.range f)

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

theorem iInter_Iic_eq_empty_iff {ι : Sort u} {α : Type v} [LinearOrder α] {f : ι → α} : ⋂ (i : ι), Set.Iic (f i) = ∅ ↔ ¬BddBelow (Set.range f)

theorem iInter_Iio_of_not_bddBelow_range {ι : Sort u} {α : Type v} [LinearOrder α] {f : ι → α} (hf : ¬BddBelow (Set.range f)) : ⋂ (i : ι), Set.Iio (f i) = ∅