Documentation

Mathlib.Algebra.Order.Ring.Finset

Finset.sup and ring operations #

@[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)
@[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)
@[simp]
theorem Nat.cast_finsetSup {ι : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [OrderBot R] [CanonicallyOrderedAdd R] (s : Finset ι) (f : ι) :
(s.sup f) = s.sup fun (i : ι) => (f i)
theorem Finset.mul_sup₀ {R : Type u_1} {ι : Type u_2} [LinearOrder R] [NonUnitalNonAssocSemiring R] [CanonicallyOrderedAdd R] [OrderBot R] (s : Finset ι) (f : ιR) (a : R) :
a * s.sup f = s.sup fun (x : ι) => a * f x
theorem Finset.sup_mul₀ {R : Type u_1} {ι : Type u_2} [LinearOrder R] [NonUnitalNonAssocSemiring R] [CanonicallyOrderedAdd R] [OrderBot R] (s : Finset ι) (f : ιR) (a : R) :
s.sup f * a = s.sup fun (x : ι) => f x * a

Also see Finset.sup'_mul₀ for a version for GroupWithZeros.