Documentation

Mathlib.Data.Set.Intervals.Disjoint

Extra lemmas about intervals #

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

@[simp]
theorem Set.Iic_disjoint_Ioi {α : Type v} [inst : Preorder α] {a : α} {b : α} (h : a b) :
@[simp]
theorem Set.Iic_disjoint_Ioc {α : Type v} [inst : Preorder α] {a : α} {b : α} {c : α} (h : a b) :
@[simp]
theorem Set.Ioc_disjoint_Ioc_same {α : Type v} [inst : Preorder α] {a : α} {b : α} {c : α} :
@[simp]
theorem Set.Ico_disjoint_Ico_same {α : Type v} [inst : Preorder α] {a : α} {b : α} {c : α} :
@[simp]
theorem Set.Ici_disjoint_Iic {α : Type v} [inst : Preorder α] {a : α} {b : α} :
@[simp]
theorem Set.Iic_disjoint_Ici {α : Type v} [inst : Preorder α] {a : α} {b : α} :
@[simp]
theorem Set.unionᵢ_Iic {α : Type v} [inst : Preorder α] :
(Set.unionᵢ fun a => Set.Iic a) = Set.univ
@[simp]
theorem Set.unionᵢ_Ici {α : Type v} [inst : Preorder α] :
(Set.unionᵢ fun a => Set.Ici a) = Set.univ
@[simp]
theorem Set.unionᵢ_Icc_right {α : Type v} [inst : Preorder α] (a : α) :
(Set.unionᵢ fun b => Set.Icc a b) = Set.Ici a
@[simp]
theorem Set.unionᵢ_Ioc_right {α : Type v} [inst : Preorder α] (a : α) :
(Set.unionᵢ fun b => Set.Ioc a b) = Set.Ioi a
@[simp]
theorem Set.unionᵢ_Icc_left {α : Type v} [inst : Preorder α] (b : α) :
(Set.unionᵢ fun a => Set.Icc a b) = Set.Iic b
@[simp]
theorem Set.unionᵢ_Ico_left {α : Type v} [inst : Preorder α] (b : α) :
(Set.unionᵢ fun a => Set.Ico a b) = Set.Iio b
@[simp]
theorem Set.unionᵢ_Iio {α : Type v} [inst : Preorder α] [inst : NoMaxOrder α] :
(Set.unionᵢ fun a => Set.Iio a) = Set.univ
@[simp]
theorem Set.unionᵢ_Ioi {α : Type v} [inst : Preorder α] [inst : NoMinOrder α] :
(Set.unionᵢ fun a => Set.Ioi a) = Set.univ
@[simp]
theorem Set.unionᵢ_Ico_right {α : Type v} [inst : Preorder α] [inst : NoMaxOrder α] (a : α) :
(Set.unionᵢ fun b => Set.Ico a b) = Set.Ici a
@[simp]
theorem Set.unionᵢ_Ioo_right {α : Type v} [inst : Preorder α] [inst : NoMaxOrder α] (a : α) :
(Set.unionᵢ fun b => Set.Ioo a b) = Set.Ioi a
@[simp]
theorem Set.unionᵢ_Ioc_left {α : Type v} [inst : Preorder α] [inst : NoMinOrder α] (b : α) :
(Set.unionᵢ fun a => Set.Ioc a b) = Set.Iic b
@[simp]
theorem Set.unionᵢ_Ioo_left {α : Type v} [inst : Preorder α] [inst : NoMinOrder α] (b : α) :
(Set.unionᵢ fun a => Set.Ioo a b) = Set.Iio b
@[simp]
theorem Set.Ico_disjoint_Ico {α : Type v} [inst : LinearOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
Disjoint (Set.Ico a₁ a₂) (Set.Ico b₁ b₂) min a₂ b₂ max a₁ b₁
@[simp]
theorem Set.Ioc_disjoint_Ioc {α : Type v} [inst : LinearOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
Disjoint (Set.Ioc a₁ a₂) (Set.Ioc b₁ b₂) min a₂ b₂ max a₁ b₁
theorem Set.eq_of_Ico_disjoint {α : Type v} [inst : LinearOrder α] {x₁ : α} {x₂ : α} {y₁ : α} {y₂ : α} (h : Disjoint (Set.Ico x₁ x₂) (Set.Ico y₁ y₂)) (hx : x₁ < x₂) (h2 : x₂ Set.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.unionᵢ_Ico_eq_Iio_self_iff {ι : Sort u} {α : Type v} [inst : LinearOrder α] {f : ια} {a : α} :
(Set.unionᵢ fun i => Set.Ico (f i) a) = Set.Iio a ∀ (x : α), x < ai, f i x
@[simp]
theorem Set.unionᵢ_Ioc_eq_Ioi_self_iff {ι : Sort u} {α : Type v} [inst : LinearOrder α] {f : ια} {a : α} :
(Set.unionᵢ fun i => Set.Ioc a (f i)) = Set.Ioi a ∀ (x : α), a < xi, x f i
@[simp]
theorem Set.bunionᵢ_Ico_eq_Iio_self_iff {ι : Sort u} {α : Type v} [inst : LinearOrder α] {p : ιProp} {f : (i : ι) → p iα} {a : α} :
(Set.unionᵢ fun i => Set.unionᵢ fun hi => Set.Ico (f i hi) a) = Set.Iio a ∀ (x : α), x < ai hi, f i hi x
@[simp]
theorem Set.bunionᵢ_Ioc_eq_Ioi_self_iff {ι : Sort u} {α : Type v} [inst : LinearOrder α] {p : ιProp} {f : (i : ι) → p iα} {a : α} :
(Set.unionᵢ fun i => Set.unionᵢ fun hi => Set.Ioc a (f i hi)) = Set.Ioi a ∀ (x : α), a < xi hi, x f i hi
theorem IsGLB.bunionᵢ_Ioi_eq {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α} (h : IsGLB s a) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => Set.Ioi x) = Set.Ioi a
theorem IsGLB.unionᵢ_Ioi_eq {ι : Sort u} {α : Type v} [inst : LinearOrder α] {a : α} {f : ια} (h : IsGLB (Set.range f) a) :
(Set.unionᵢ fun x => Set.Ioi (f x)) = Set.Ioi a
theorem IsLUB.bunionᵢ_Iio_eq {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α} (h : IsLUB s a) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => Set.Iio x) = Set.Iio a
theorem IsLUB.unionᵢ_Iio_eq {ι : Sort u} {α : Type v} [inst : LinearOrder α] {a : α} {f : ια} (h : IsLUB (Set.range f) a) :
(Set.unionᵢ fun x => Set.Iio (f x)) = Set.Iio a
theorem IsGLB.bunionᵢ_Ici_eq_Ioi {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α} (a_glb : IsGLB s a) (a_not_mem : ¬a s) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => Set.Ici x) = Set.Ioi a
theorem IsGLB.bunionᵢ_Ici_eq_Ici {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α} (a_glb : IsGLB s a) (a_mem : a s) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => Set.Ici x) = Set.Ici a
theorem IsLUB.bunionᵢ_Iic_eq_Iio {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α} (a_lub : IsLUB s a) (a_not_mem : ¬a s) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => Set.Iic x) = Set.Iio a
theorem IsLUB.bunionᵢ_Iic_eq_Iic {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α} (a_lub : IsLUB s a) (a_mem : a s) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => Set.Iic x) = Set.Iic a
theorem unionᵢ_Ici_eq_Ioi_infᵢ {ι : Sort u} {R : Type u_1} [inst : CompleteLinearOrder R] {f : ιR} (no_least_elem : ¬(i, f i) Set.range f) :
(Set.unionᵢ fun i => Set.Ici (f i)) = Set.Ioi (i, f i)
theorem unionᵢ_Iic_eq_Iio_supᵢ {ι : Sort u} {R : Type u_1} [inst : CompleteLinearOrder R] {f : ιR} (no_greatest_elem : ¬(i, f i) Set.range f) :
(Set.unionᵢ fun i => Set.Iic (f i)) = Set.Iio (i, f i)
theorem unionᵢ_Ici_eq_Ici_infᵢ {ι : Sort u} {R : Type u_1} [inst : CompleteLinearOrder R] {f : ιR} (has_least_elem : (i, f i) Set.range f) :
(Set.unionᵢ fun i => Set.Ici (f i)) = Set.Ici (i, f i)
theorem unionᵢ_Iic_eq_Iic_supᵢ {ι : Sort u} {R : Type u_1} [inst : CompleteLinearOrder R] {f : ιR} (has_greatest_elem : (i, f i) Set.range f) :
(Set.unionᵢ fun i => Set.Iic (f i)) = Set.Iic (i, f i)