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