HepLean Documentation

Mathlib.Order.Interval.Set.Disjoint

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 (Set.Iic a) (Set.Ioi b)
source
@[simp]
theorem Set.Iio_disjoint_Ici {α : Type v} [Preorder α] {a : α} {b : α} (h : a ≤ b) :
Disjoint (Set.Iio a) (Set.Ici b)
source
@[simp]
theorem Set.Iic_disjoint_Ioc {α : Type v} [Preorder α] {a : α} {b : α} {c : α} (h : a ≤ b) :
Disjoint (Set.Iic a) (Set.Ioc b c)
source
@[simp]
theorem Set.Ioc_disjoint_Ioc_same {α : Type v} [Preorder α] {a : α} {b : α} {c : α} :
Disjoint (Set.Ioc a b) (Set.Ioc b c)
source
@[simp]
theorem Set.Ico_disjoint_Ico_same {α : Type v} [Preorder α] {a : α} {b : α} {c : α} :
Disjoint (Set.Ico a b) (Set.Ico b c)
source
@[simp]
theorem Set.Ici_disjoint_Iic {α : Type v} [Preorder α] {a : α} {b : α} :
Disjoint (Set.Ici a) (Set.Iic b) ↔ ¬a ≤ b
source
@[simp]
theorem Set.Iic_disjoint_Ici {α : Type v} [Preorder α] {a : α} {b : α} :
Disjoint (Set.Iic a) (Set.Ici b) ↔ ¬b ≤ a
source
@[simp]
theorem Set.Ioc_disjoint_Ioi {α : Type v} [Preorder α] {a : α} {b : α} {c : α} (h : b ≤ c) :
Disjoint (Set.Ioc a b) (Set.Ioi c)
source
theorem Set.Ioc_disjoint_Ioi_same {α : Type v} [Preorder α] {a : α} {b : α} :
Disjoint (Set.Ioc a b) (Set.Ioi b)
source
@[simp]
theorem Set.iUnion_Iic {α : Type v} [Preorder α] :
⋃ (a : α), Set.Iic a = Set.univ
source
@[simp]
theorem Set.iUnion_Ici {α : Type v} [Preorder α] :
⋃ (a : α), Set.Ici a = Set.univ
source
@[simp]
theorem Set.iUnion_Icc_right {α : Type v} [Preorder α] (a : α) :
⋃ (b : α), Set.Icc a b = Set.Ici a
source
@[simp]
theorem Set.iUnion_Ioc_right {α : Type v} [Preorder α] (a : α) :
⋃ (b : α), Set.Ioc a b = Set.Ioi a
source
@[simp]
theorem Set.iUnion_Icc_left {α : Type v} [Preorder α] (b : α) :
⋃ (a : α), Set.Icc a b = Set.Iic b
source
@[simp]
theorem Set.iUnion_Ico_left {α : Type v} [Preorder α] (b : α) :
⋃ (a : α), Set.Ico a b = Set.Iio b
source
@[simp]
theorem Set.iUnion_Iio {α : Type v} [Preorder α] [NoMaxOrder α] :
⋃ (a : α), Set.Iio a = Set.univ
source
@[simp]
theorem Set.iUnion_Ioi {α : Type v} [Preorder α] [NoMinOrder α] :
⋃ (a : α), Set.Ioi a = Set.univ
source
@[simp]
theorem Set.iUnion_Ico_right {α : Type v} [Preorder α] [NoMaxOrder α] (a : α) :
⋃ (b : α), Set.Ico a b = Set.Ici a
source
@[simp]
theorem Set.iUnion_Ioo_right {α : Type v} [Preorder α] [NoMaxOrder α] (a : α) :
⋃ (b : α), Set.Ioo a b = Set.Ioi a
source
@[simp]
theorem Set.iUnion_Ioc_left {α : Type v} [Preorder α] [NoMinOrder α] (b : α) :
⋃ (a : α), Set.Ioc a b = Set.Iic b
source
@[simp]
theorem Set.iUnion_Ioo_left {α : Type v} [Preorder α] [NoMinOrder α] (b : α) :
⋃ (a : α), Set.Ioo a b = Set.Iio b
source
@[simp]
theorem Set.Ico_disjoint_Ico {α : Type v} [LinearOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
Disjoint (Set.Ico a₁ a₂) (Set.Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
source
@[simp]
theorem Set.Ioc_disjoint_Ioc {α : Type v} [LinearOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
Disjoint (Set.Ioc a₁ a₂) (Set.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 (Set.Ioo a₁ a₂) (Set.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 (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.

source
@[simp]
theorem Set.iUnion_Ico_eq_Iio_self_iff {ι : Sort u} {α : Type v} [LinearOrder α] {f : ι → α} {a : α} :
⋃ (i : ι), Set.Ico (f i) a = Set.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 : ι), Set.Ioc a (f i) = Set.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), Set.Ico (f i hi) a = Set.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), Set.Ioc a (f i hi) = Set.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_not_mem : 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_not_mem : 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) = ∅