∀ {ι : Type u_1} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f g f' g' : (i : ι) → π i}
  [inst_1 : (i : ι) → Preorder (π i)], f ≤ f' → g ≤ g' → s.piecewise f g ≤ s.piecewise f' g'