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.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
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 : α}
:
@[simp]
theorem
Set.unionᵢ_Ioc_eq_Ioi_self_iff
{ι : Sort u}
{α : Type v}
[inst : LinearOrder α]
{f : ι → α}
{a : α}
:
@[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 < a → ∃ i 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 < x → ∃ i 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)