Algebraic properties of finitary supremum

theorem Finset.sup_mul_le_mul_sup_of_nonneg {ι : Type u_1} {R : Type u_2} [LinearOrderedSemiring R] {a : ι → R} {b : ι → R} [OrderBot R] (s : Finset ι) (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : s.sup (a * b) ≤ s.sup a * s.sup b

theorem Finset.mul_inf_le_inf_mul_of_nonneg {ι : Type u_1} {R : Type u_2} [LinearOrderedSemiring R] {a : ι → R} {b : ι → R} [OrderTop R] (s : Finset ι) (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : s.inf a * s.inf b ≤ s.inf (a * b)

theorem Finset.sup'_mul_le_mul_sup'_of_nonneg {ι : Type u_1} {R : Type u_2} [LinearOrderedSemiring R] {a : ι → R} {b : ι → R} (s : Finset ι) (H : s.Nonempty) (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : s.sup' H (a * b) ≤ s.sup' H a * s.sup' H b

theorem Finset.inf'_mul_le_mul_inf'_of_nonneg {ι : Type u_1} {R : Type u_2} [LinearOrderedSemiring R] {a : ι → R} {b : ι → R} (s : Finset ι) (H : s.Nonempty) (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : s.inf' H a * s.inf' H b ≤ s.inf' H (a * b)