Finset.sup of Nat.cast #
@[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)
@[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)
@[simp]
theorem
Nat.cast_finsetSup
{ι : Type u_1}
{R : Type u_2}
[CanonicallyLinearOrderedSemifield R]
(s : Finset ι)
(f : ι → ℕ)
:
↑(s.sup f) = s.sup fun (i : ι) => ↑(f i)