feat(data/indicator_function): add indicator_range_comp (#3343)

Add
* `comp_eq_of_eq_on_range`;
* `piecewise_eq_on`;
* `piecewise_eq_on_compl`;
* `piecewise_compl`;
* `piecewise_range_comp`;
* `indicator_range_comp`.

Author: urkud

src/data/indicator_function.lean

@@ -51,6 +51,10 @@ lemma eq_on_indicator : eq_on (indicator s f) f s := λ x hx, indicator_of_mem h
 lemma support_indicator : function.support (s.indicator f) ⊆ s :=
 λ x hx, hx.imp_symm (λ h, indicator_of_not_mem h f)
 
+@[simp] lemma indicator_range_comp {ι : Sort*} (f : ι → α) (g : α → β) :
+  indicator (range f) g ∘ f = g ∘ f :=
+piecewise_range_comp _ _ _
+
 lemma indicator_congr (h : ∀ a ∈ s, f a = g a) : indicator s f = indicator s g :=
 funext $ λx, by { simp only [indicator], split_ifs, { exact h _ h_1 }, refl }
 
@@ -203,7 +207,7 @@ by { rw indicator_apply, split_ifs with as, { exact h as }, refl }
 lemma indicator_nonpos (h : ∀ a ∈ s, f a ≤ 0) : ∀ a, indicator s f a ≤ 0 :=
 λ a, indicator_nonpos' (h a)
 
-lemma indicator_le_indicator (h : f a ≤ g a) : indicator s f a ≤ indicator s g a :=
+@[mono] lemma indicator_le_indicator (h : f a ≤ g a) : indicator s f a ≤ indicator s g a :=
 by { simp only [indicator], split_ifs with ha, { exact h }, refl }
 
 lemma indicator_le_indicator_of_subset (h : s ⊆ t) (hf : ∀a, 0 ≤ f a) (a : α) :

src/data/set/function.lean

@@ -88,6 +88,10 @@ image_congr heq
 lemma eq_on.mono (hs : s₁ ⊆ s₂) (hf : eq_on f₁ f₂ s₂) : eq_on f₁ f₂ s₁ :=
 λ x hx, hf (hs hx)
 
+lemma comp_eq_of_eq_on_range {ι : Sort*} {f : ι → α} {g₁ g₂ : α → β} (h : eq_on g₁ g₂ (range f)) :
+  g₁ ∘ f = g₂ ∘ f :=
+funext $ λ x, h $ mem_range_self _
+
 /-! ### maps to -/
 
 /-- `maps_to f a b` means that the image of `a` is contained in `b`. -/
@@ -443,11 +447,25 @@ by simp [piecewise, hi]
 lemma piecewise_eq_of_not_mem {i : α} (hi : i ∉ s) : s.piecewise f g i = g i :=
 by simp [piecewise, hi]
 
+lemma piecewise_eq_on (f g : α → β) : eq_on (s.piecewise f g) f s :=
+λ _, piecewise_eq_of_mem _ _ _
+
+lemma piecewise_eq_on_compl (f g : α → β) : eq_on (s.piecewise f g) g sᶜ :=
+λ _, piecewise_eq_of_not_mem _ _ _
+
 @[simp, priority 990]
 lemma piecewise_insert_of_ne {i j : α} (h : i ≠ j) [∀i, decidable (i ∈ insert j s)] :
   (insert j s).piecewise f g i = s.piecewise f g i :=
 by simp [piecewise, h]
 
+@[simp] lemma piecewise_compl [∀ i, decidable (i ∈ sᶜ)] : sᶜ.piecewise f g = s.piecewise g f :=
+funext $ λ x, if hx : x ∈ s then by simp [hx] else by simp [hx]
+
+@[simp] lemma piecewise_range_comp {ι : Sort*} (f : ι → α) [Π j, decidable (j ∈ range f)]
+  (g₁ g₂ : α → β) :
+  (range f).piecewise g₁ g₂ ∘ f = g₁ ∘ f :=
+comp_eq_of_eq_on_range $ piecewise_eq_on _ _ _
+
 end set
 
 namespace function