Extra lemmas about intervals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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.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.Union_Iic {α : Type v} [preorder α] :

(⋃ (a : α), set.Iic a) = set.univ

source

@[simp]

theorem set.Union_Ici {α : Type v} [preorder α] :

(⋃ (a : α), set.Ici a) = set.univ

source

@[simp]

theorem set.Union_Icc_right {α : Type v} [preorder α] (a : α) :

(⋃ (b : α), set.Icc a b) = set.Ici a

source

@[simp]

theorem set.Union_Ioc_right {α : Type v} [preorder α] (a : α) :

(⋃ (b : α), set.Ioc a b) = set.Ioi a

source

@[simp]

theorem set.Union_Icc_left {α : Type v} [preorder α] (b : α) :

(⋃ (a : α), set.Icc a b) = set.Iic b

source

@[simp]

theorem set.Union_Ico_left {α : Type v} [preorder α] (b : α) :

(⋃ (a : α), set.Ico a b) = set.Iio b

source

@[simp]

theorem set.Union_Iio {α : Type v} [preorder α] [no_max_order α] :

(⋃ (a : α), set.Iio a) = set.univ

source

@[simp]

theorem set.Union_Ioi {α : Type v} [preorder α] [no_min_order α] :

(⋃ (a : α), set.Ioi a) = set.univ

source

@[simp]

theorem set.Union_Ico_right {α : Type v} [preorder α] [no_max_order α] (a : α) :

(⋃ (b : α), set.Ico a b) = set.Ici a

source

@[simp]

theorem set.Union_Ioo_right {α : Type v} [preorder α] [no_max_order α] (a : α) :

(⋃ (b : α), set.Ioo a b) = set.Ioi a

source

@[simp]

theorem set.Union_Ioc_left {α : Type v} [preorder α] [no_min_order α] (b : α) :

(⋃ (a : α), set.Ioc a b) = set.Iic b

source

@[simp]

theorem set.Union_Ioo_left {α : Type v} [preorder α] [no_min_order α] (b : α) :

(⋃ (a : α), set.Ioo a b) = set.Iio b

source

@[simp]

theorem set.Ico_disjoint_Ico {α : Type v} [linear_order α] {a₁ a₂ b₁ b₂ : α} :

disjoint (set.Ico a₁ a₂) (set.Ico b₁ b₂) ↔ linear_order.min a₂ b₂ ≤ linear_order.max a₁ b₁

source

@[simp]

theorem set.Ioc_disjoint_Ioc {α : Type v} [linear_order α] {a₁ a₂ b₁ b₂ : α} :

disjoint (set.Ioc a₁ a₂) (set.Ioc b₁ b₂) ↔ linear_order.min a₂ b₂ ≤ linear_order.max a₁ b₁

source

theorem set.eq_of_Ico_disjoint {α : Type v} [linear_order α] {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.Union_Ico_eq_Iio_self_iff {ι : Sort u} {α : Type v} [linear_order α] {f : ι → α} {a : α} :

(⋃ (i : ι), set.Ico (f i) a) = set.Iio a ↔ ∀ (x : α), x < a → (∃ (i : ι), f i ≤ x)

source

@[simp]

theorem set.Union_Ioc_eq_Ioi_self_iff {ι : Sort u} {α : Type v} [linear_order α] {f : ι → α} {a : α} :

(⋃ (i : ι), set.Ioc a (f i)) = set.Ioi a ↔ ∀ (x : α), a < x → (∃ (i : ι), x ≤ f i)

source

@[simp]

theorem set.bUnion_Ico_eq_Iio_self_iff {ι : Sort u} {α : Type v} [linear_order α] {p : ι → Prop} {f : Π (i : ι), p i → α} {a : α} :

(⋃ (i : ι) (hi : p i), set.Ico (f i hi) a) = set.Iio a ↔ ∀ (x : α), x < a → (∃ (i : ι) (hi : p i), f i hi ≤ x)

source

@[simp]

theorem set.bUnion_Ioc_eq_Ioi_self_iff {ι : Sort u} {α : Type v} [linear_order α] {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 is_glb.bUnion_Ioi_eq {α : Type v} [linear_order α] {s : set α} {a : α} (h : is_glb s a) :

(⋃ (x : α) (H : x ∈ s), set.Ioi x) = set.Ioi a

source

theorem is_glb.Union_Ioi_eq {ι : Sort u} {α : Type v} [linear_order α] {a : α} {f : ι → α} (h : is_glb (set.range f) a) :

(⋃ (x : ι), set.Ioi (f x)) = set.Ioi a

source

theorem is_lub.bUnion_Iio_eq {α : Type v} [linear_order α] {s : set α} {a : α} (h : is_lub s a) :

(⋃ (x : α) (H : x ∈ s), set.Iio x) = set.Iio a

source

theorem is_lub.Union_Iio_eq {ι : Sort u} {α : Type v} [linear_order α] {a : α} {f : ι → α} (h : is_lub (set.range f) a) :

(⋃ (x : ι), set.Iio (f x)) = set.Iio a

source

theorem is_glb.bUnion_Ici_eq_Ioi {α : Type v} [linear_order α] {s : set α} {a : α} (a_glb : is_glb s a) (a_not_mem : a ∉ s) :

(⋃ (x : α) (H : x ∈ s), set.Ici x) = set.Ioi a

source

theorem is_glb.bUnion_Ici_eq_Ici {α : Type v} [linear_order α] {s : set α} {a : α} (a_glb : is_glb s a) (a_mem : a ∈ s) :

(⋃ (x : α) (H : x ∈ s), set.Ici x) = set.Ici a

source

theorem is_lub.bUnion_Iic_eq_Iio {α : Type v} [linear_order α] {s : set α} {a : α} (a_lub : is_lub s a) (a_not_mem : a ∉ s) :

(⋃ (x : α) (H : x ∈ s), set.Iic x) = set.Iio a

source

theorem is_lub.bUnion_Iic_eq_Iic {α : Type v} [linear_order α] {s : set α} {a : α} (a_lub : is_lub s a) (a_mem : a ∈ s) :

(⋃ (x : α) (H : x ∈ s), set.Iic x) = set.Iic a

source

theorem Union_Ici_eq_Ioi_infi {ι : Sort u} {R : Type u_1} [complete_linear_order R] {f : ι → R} (no_least_elem : (⨅ (i : ι), f i) ∉ set.range f) :

(⋃ (i : ι), set.Ici (f i)) = set.Ioi (⨅ (i : ι), f i)

source

theorem Union_Iic_eq_Iio_supr {ι : Sort u} {R : Type u_1} [complete_linear_order R] {f : ι → R} (no_greatest_elem : (⨆ (i : ι), f i) ∉ set.range f) :

(⋃ (i : ι), set.Iic (f i)) = set.Iio (⨆ (i : ι), f i)

source

theorem Union_Ici_eq_Ici_infi {ι : Sort u} {R : Type u_1} [complete_linear_order R] {f : ι → R} (has_least_elem : (⨅ (i : ι), f i) ∈ set.range f) :

(⋃ (i : ι), set.Ici (f i)) = set.Ici (⨅ (i : ι), f i)

source

theorem Union_Iic_eq_Iic_supr {ι : Sort u} {R : Type u_1} [complete_linear_order R] {f : ι → R} (has_greatest_elem : (⨆ (i : ι), f i) ∈ set.range f) :

(⋃ (i : ι), set.Iic (f i)) = set.Iic (⨆ (i : ι), f i)