Documentation

Mathlib.Algebra.Order.Ring.Finset

Finset.sup of Nat.cast #

source
@[simp]
theorem Nat.cast_finsetSup' {ι : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [CanonicallyOrderedAdd R] (s : Finset ι) (f : ι → ℕ) :
↑(s.sup f) = s.sup fun (i : ι) => ↑(f i)