Documentation
Carleson
.
ToMathlib
.
Order
.
Interval
.
Set
.
Disjoint
Search
return to top
source
Imports
Init
Mathlib.Order.Interval.Set.Disjoint
Imported by
iUnion_Icc_eq_Ici_self_iff
IsGLB
.
biUnion_Ioi_eq_Ioi
iUnion_Ioi_eq_Ioi_iInf
iUnion_Iio_eq_Iio_iSup
source
@[simp]
theorem
iUnion_Icc_eq_Ici_self_iff
{
ι
:
Sort
u_1}
{
α
:
Type
u_2}
[
LinearOrder
α
]
{
f
:
ι
→
α
}
{
a
:
α
}
:
⋃ (
i
:
ι
),
Set.Icc
a
(
f
i
)
=
Set.Ici
a
↔
∀ (
x
:
α
),
a
≤
x
→
∃ (
i
:
ι
),
x
≤
f
i
source
theorem
IsGLB
.
biUnion_Ioi_eq_Ioi
{
α
:
Type
u_1}
[
LinearOrder
α
]
{
s
:
Set
α
}
{
a
:
α
}
(
a_glb
:
IsGLB
s
a
)
:
⋃
x
∈
s
,
Set.Ioi
x
=
Set.Ioi
a
source
theorem
iUnion_Ioi_eq_Ioi_iInf
{
ι
:
Sort
u_1}
{
R
:
Type
u_2}
[
CompleteLinearOrder
R
]
{
f
:
ι
→
R
}
:
⋃ (
i
:
ι
),
Set.Ioi
(
f
i
)
=
Set.Ioi
(⨅ (
i
:
ι
),
f
i
)
source
theorem
iUnion_Iio_eq_Iio_iSup
{
ι
:
Sort
u_1}
{
R
:
Type
u_2}
[
CompleteLinearOrder
R
]
{
f
:
ι
→
R
}
:
⋃ (
i
:
ι
),
Set.Iio
(
f
i
)
=
Set.Iio
(⨆ (
i
:
ι
),
f
i
)