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]
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.
@[simp]
theorem
set.Union_Ico_eq_Iio_self_iff
{ι : Sort u}
{α : Type v}
[linear_order α]
{f : ι → α}
{a : α} :
@[simp]
theorem
set.Union_Ioc_eq_Ioi_self_iff
{ι : Sort u}
{α : Type v}
[linear_order α]
{f : ι → α}
{a : α} :
@[simp]
theorem
set.bUnion_Ico_eq_Iio_self_iff
{ι : Sort u}
{α : Type v}
[linear_order α]
{p : ι → Prop}
{f : Π (i : ι), p i → α}
{a : α} :
@[simp]
theorem
set.bUnion_Ioc_eq_Ioi_self_iff
{ι : Sort u}
{α : Type v}
[linear_order α]
{p : ι → Prop}
{f : Π (i : ι), p i → α}
{a : α} :
theorem
is_glb.Union_Ioi_eq
{ι : Sort u}
{α : Type v}
[linear_order α]
{a : α}
{f : ι → α}
(h : is_glb (set.range f) a) :
theorem
is_lub.Union_Iio_eq
{ι : Sort u}
{α : Type v}
[linear_order α]
{a : α}
{f : ι → α}
(h : is_lub (set.range f) a) :