Documentation
Mathlib
.
Algebra
.
Order
.
Ring
.
Finset
Search
return to top
source
Imports
Init
Mathlib.Data.Finset.Lattice.Fold
Mathlib.Data.Nat.Cast.Order.Ring
Imported by
Nat
.
cast_finsetSup'
Nat
.
cast_finsetInf'
Nat
.
cast_finsetSup
Finset.sup
of
Nat.cast
#
source
@[simp]
theorem
Nat
.
cast_finsetSup'
{ι :
Type
u_1}
{R :
Type
u_2}
[
LinearOrderedSemiring
R
]
{s :
Finset
ι
}
(f :
ι
→
ℕ
)
(hs :
s
.
Nonempty
)
:
↑
(
s
.
sup'
hs
f
)
=
s
.
sup'
hs
fun (
i
:
ι
) =>
↑
(
f
i
)
source
@[simp]
theorem
Nat
.
cast_finsetInf'
{ι :
Type
u_1}
{R :
Type
u_2}
[
LinearOrderedSemiring
R
]
{s :
Finset
ι
}
(f :
ι
→
ℕ
)
(hs :
s
.
Nonempty
)
:
↑
(
s
.
inf'
hs
f
)
=
s
.
inf'
hs
fun (
i
:
ι
) =>
↑
(
f
i
)
source
@[simp]
theorem
Nat
.
cast_finsetSup
{ι :
Type
u_1}
{R :
Type
u_2}
[
LinearOrderedSemiring
R
]
[
CanonicallyOrderedAdd
R
]
(s :
Finset
ι
)
(f :
ι
→
ℕ
)
:
↑
(
s
.
sup
f
)
=
s
.
sup
fun (
i
:
ι
) =>
↑
(
f
i
)