Documentation
Mathlib
.
Data
.
ENat
.
BigOperators
Search
return to top
source
Imports
Init
Mathlib.Data.ENat.Lattice
Mathlib.Algebra.Order.BigOperators.Group.Finset
Imported by
ENat
.
sum_iSup
ENat
.
sum_iSup_of_monotone
Sum of suprema in
ENat
#
source
theorem
ENat
.
sum_iSup
{
α
:
Type
u_1}
{
ι
:
Type
u_2}
{
s
:
Finset
α
}
{
f
:
α
→
ι
→
ENat
}
(
hf
:
∀ (
i
j
:
ι
),
Exists
fun (
k
:
ι
) =>
∀ (
a
:
α
),
And
(
LE.le
(
f
a
i
)
(
f
a
k
)
)
(
LE.le
(
f
a
j
)
(
f
a
k
)
)
)
:
Eq
(
s
.
sum
fun (
a
:
α
) =>
iSup
fun (
i
:
ι
) =>
f
a
i
)
(
iSup
fun (
i
:
ι
) =>
s
.
sum
fun (
a
:
α
) =>
f
a
i
)
source
theorem
ENat
.
sum_iSup_of_monotone
{
α
:
Type
u_1}
{
ι
:
Type
u_2}
[
Preorder
ι
]
[
IsDirected
ι
fun (
x1
x2
:
ι
) =>
LE.le
x1
x2
]
{
s
:
Finset
α
}
{
f
:
α
→
ι
→
ENat
}
(
hf
:
∀ (
a
:
α
),
Monotone
(
f
a
)
)
:
Eq
(
s
.
sum
fun (
a
:
α
) =>
iSup
(
f
a
)
)
(
iSup
fun (
n
:
ι
) =>
s
.
sum
fun (
a
:
α
) =>
f
a
n
)