∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M]
  [inst_2 : AddCommMonoid N] [inst_3 : PartialOrder N] [IsOrderedAddMonoid N] [inst_5 : Module ℚ≥0 N]
  [PosSMulMono ℚ≥0 N] {m : M → N} {p : M → Prop} {f : ι → M} {s : Finset ι},
  m 0 = 0 →
    (∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b) →
      (∀ (a b : M), p a → p b → p (a + b)) →
        (∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a) →
          (∀ i ∈ s, p (f i)) → m (s.expect fun i => f i) ≤ s.expect fun i => m (f i)