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