feat(data/finset/basic): add finset.piecewise_le_piecewise (#5572)

* add `finset.piecewise_le_piecewise` and `finset.piecewise_le_piecewise'`;
* add `finset.piecewise_compl`.

src/algebra/linear_ordered_comm_group_with_zero.lean

@@ -43,7 +43,6 @@ instance linear_ordered_comm_group_with_zero.to_ordered_comm_monoid : ordered_co
     exact linear_ordered_comm_group_with_zero.mul_le_mul_left h a }
   .. ‹linear_ordered_comm_group_with_zero α› }
 
-
 section linear_ordered_comm_monoid
 /-
 The following facts are true more generally in a (linearly) ordered commutative monoid.

src/data/finset/basic.lean

@@ -1033,6 +1033,14 @@ lemma le_piecewise_of_le_of_le {δ : α → Type*} [Π i, preorder (δ i)] {f g
   (Hf : h ≤ f) (Hg : h ≤ g) : h ≤ s.piecewise f g :=
 λ x, piecewise_cases s f g (λ y, h x ≤ y) (Hf x) (Hg x)
 
+lemma piecewise_le_piecewise' {δ : α → Type*} [Π i, preorder (δ i)] {f g f' g' : Π i, δ i}
+  (Hf : ∀ x ∈ s, f x ≤ f' x) (Hg : ∀ x ∉ s, g x ≤ g' x) : s.piecewise f g ≤ s.piecewise f' g' :=
+λ x, by { by_cases hx : x ∈ s; simp [hx, *] }
+
+lemma piecewise_le_piecewise {δ : α → Type*} [Π i, preorder (δ i)] {f g f' g' : Π i, δ i}
+  (Hf : f ≤ f') (Hg : g ≤ g') : s.piecewise f g ≤ s.piecewise f' g' :=
+s.piecewise_le_piecewise' (λ x _, Hf x) (λ x _, Hg x)
+
 lemma piecewise_mem_Icc_of_mem_of_mem {δ : α → Type*} [Π i, preorder (δ i)] {f f₁ g g₁ : Π i, δ i}
   (hf : f ∈ set.Icc f₁ g₁) (hg : g ∈ set.Icc f₁ g₁) :
   s.piecewise f g ∈ set.Icc f₁ g₁ :=

src/data/fintype/basic.lean

@@ -90,6 +90,11 @@ by rw [inter_comm, univ_inter]
   {δ : α → Sort*} (f g : Πi, δ i) : univ.piecewise f g = f :=
 by { ext i, simp [piecewise] }
 
+lemma piecewise_compl [decidable_eq α] (s : finset α) [Π i : α, decidable (i ∈ s)]
+  [Π i : α, decidable (i ∈ sᶜ)] {δ : α → Sort*} (f g : Π i, δ i) :
+  sᶜ.piecewise f g = s.piecewise g f :=
+by { ext i, simp [piecewise] }
+
 lemma univ_map_equiv_to_embedding {α β : Type*} [fintype α] [fintype β] (e : α ≃ β) :
   univ.map e.to_embedding = univ :=
 begin