# Functions defined piecewise on a finset #

This file defines Finset.piecewise: Given two functions f, g, s.piecewise f g is a function which is equal to f on s and g on the complement.

## TODO #

Should we deduplicate this from Set.piecewise?

def Finset.piecewise {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j s)] (i : ι) :
π i

s.piecewise f g is the function equal to f on the finset s, and to g on its complement.

Equations
• s.piecewise f g i = if i s then f i else g i
Instances For
theorem Finset.piecewise_insert_self {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [] {j : ι} [(i : ι) → Decidable (i insert j s)] :
(insert j s).piecewise f g j = f j
@[simp]
theorem Finset.piecewise_empty {ι : Type u_1} {π : ιSort u_2} (f : (i : ι) → π i) (g : (i : ι) → π i) [(i : ι) → Decidable (i )] :
.piecewise f g = g
theorem Finset.piecewise_coe {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j s)] [(j : ι) → Decidable (j s)] :
(↑s).piecewise f g = s.piecewise f g
@[simp]
theorem Finset.piecewise_eq_of_mem {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j s)] {i : ι} (hi : i s) :
s.piecewise f g i = f i
@[simp]
theorem Finset.piecewise_eq_of_not_mem {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j s)] {i : ι} (hi : is) :
s.piecewise f g i = g i
theorem Finset.piecewise_congr {ι : Type u_1} {π : ιSort u_2} (s : ) [(j : ι) → Decidable (j s)] {f : (i : ι) → π i} {f' : (i : ι) → π i} {g : (i : ι) → π i} {g' : (i : ι) → π i} (hf : is, f i = f' i) (hg : is, g i = g' i) :
s.piecewise f g = s.piecewise f' g'
@[simp]
theorem Finset.piecewise_insert_of_ne {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j s)] [] {i : ι} {j : ι} [(i : ι) → Decidable (i insert j s)] (h : i j) :
(insert j s).piecewise f g i = s.piecewise f g i
theorem Finset.piecewise_insert {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j s)] [] (j : ι) [(i : ι) → Decidable (i insert j s)] :
(insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j)
theorem Finset.piecewise_cases {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j s)] {i : ι} (p : π iProp) (hf : p (f i)) (hg : p (g i)) :
p (s.piecewise f g i)
theorem Finset.piecewise_singleton {ι : Type u_1} {π : ιSort u_2} (f : (i : ι) → π i) (g : (i : ι) → π i) [] (i : ι) :
{i}.piecewise f g = Function.update g i (f i)
theorem Finset.piecewise_piecewise_of_subset_left {ι : Type u_1} {π : ιSort u_2} {s : } {t : } [(i : ι) → Decidable (i s)] [(i : ι) → Decidable (i t)] (h : s t) (f₁ : (a : ι) → π a) (f₂ : (a : ι) → π a) (g : (a : ι) → π a) :
s.piecewise (t.piecewise f₁ f₂) g = s.piecewise f₁ g
@[simp]
theorem Finset.piecewise_idem_left {ι : Type u_1} {π : ιSort u_2} (s : ) [(j : ι) → Decidable (j s)] (f₁ : (a : ι) → π a) (f₂ : (a : ι) → π a) (g : (a : ι) → π a) :
s.piecewise (s.piecewise f₁ f₂) g = s.piecewise f₁ g
theorem Finset.piecewise_piecewise_of_subset_right {ι : Type u_1} {π : ιSort u_2} {s : } {t : } [(i : ι) → Decidable (i s)] [(i : ι) → Decidable (i t)] (h : t s) (f : (a : ι) → π a) (g₁ : (a : ι) → π a) (g₂ : (a : ι) → π a) :
s.piecewise f (t.piecewise g₁ g₂) = s.piecewise f g₂
@[simp]
theorem Finset.piecewise_idem_right {ι : Type u_1} {π : ιSort u_2} (s : ) [(j : ι) → Decidable (j s)] (f : (a : ι) → π a) (g₁ : (a : ι) → π a) (g₂ : (a : ι) → π a) :
s.piecewise f (s.piecewise g₁ g₂) = s.piecewise f g₂
theorem Finset.update_eq_piecewise {ι : Type u_1} {β : Type u_3} [] (f : ιβ) (i : ι) (v : β) :
= {i}.piecewise (fun (x : ι) => v) f
theorem Finset.update_piecewise {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j s)] [] (i : ι) (v : π i) :
Function.update (s.piecewise f g) i v = s.piecewise (Function.update f i v) (Function.update g i v)
theorem Finset.update_piecewise_of_mem {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j s)] [] {i : ι} (hi : i s) (v : π i) :
Function.update (s.piecewise f g) i v = s.piecewise (Function.update f i v) g
theorem Finset.update_piecewise_of_not_mem {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) (g : (i : ι) → π i) [(j : ι) → Decidable (j s)] [] {i : ι} (hi : is) (v : π i) :
Function.update (s.piecewise f g) i v = s.piecewise f (Function.update g i v)
theorem Finset.piecewise_same {ι : Type u_1} {π : ιSort u_2} (s : ) (f : (i : ι) → π i) [(j : ι) → Decidable (j s)] :
s.piecewise f f = f
@[simp]
theorem Finset.piecewise_univ {ι : Type u_1} {π : ιSort u_2} [] [(i : ι) → Decidable (i Finset.univ)] (f : (i : ι) → π i) (g : (i : ι) → π i) :
Finset.univ.piecewise f g = f
theorem Finset.piecewise_compl {ι : Type u_1} {π : ιSort u_2} [] [] (s : ) [(i : ι) → Decidable (i s)] [(i : ι) → Decidable (i s)] (f : (i : ι) → π i) (g : (i : ι) → π i) :
s.piecewise f g = s.piecewise g f
@[simp]
theorem Finset.piecewise_erase_univ {ι : Type u_1} {π : ιSort u_2} [] [] (i : ι) (f : (i : ι) → π i) (g : (i : ι) → π i) :
(Finset.univ.erase i).piecewise f g = Function.update f i (g i)
theorem Finset.piecewise_mem_set_pi {ι : Type u_1} (s : ) [(j : ι) → Decidable (j s)] {π : ιType u_3} {t : Set ι} {t' : (i : ι) → Set (π i)} {f : (i : ι) → π i} {g : (i : ι) → π i} (hf : f t.pi t') (hg : g t.pi t') :
s.piecewise f g t.pi t'
theorem Finset.piecewise_le_of_le_of_le {ι : Type u_1} (s : ) [(j : ι) → Decidable (j s)] {π : ιType u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} {h : (i : ι) → π i} [(i : ι) → Preorder (π i)] (hf : f h) (hg : g h) :
s.piecewise f g h
theorem Finset.le_piecewise_of_le_of_le {ι : Type u_1} (s : ) [(j : ι) → Decidable (j s)] {π : ιType u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} {h : (i : ι) → π i} [(i : ι) → Preorder (π i)] (hf : h f) (hg : h g) :
h s.piecewise f g
theorem Finset.piecewise_le_piecewise' {ι : Type u_1} (s : ) [(j : ι) → Decidable (j s)] {π : ιType u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} {f' : (i : ι) → π i} {g' : (i : ι) → π i} [(i : ι) → Preorder (π i)] (hf : xs, f x f' x) (hg : xs, g x g' x) :
s.piecewise f g s.piecewise f' g'
theorem Finset.piecewise_le_piecewise {ι : Type u_1} (s : ) [(j : ι) → Decidable (j s)] {π : ιType u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} {f' : (i : ι) → π i} {g' : (i : ι) → π i} [(i : ι) → Preorder (π i)] (hf : f f') (hg : g g') :
s.piecewise f g s.piecewise f' g'
theorem Finset.piecewise_mem_Icc_of_mem_of_mem {ι : Type u_1} (s : ) [(j : ι) → Decidable (j s)] {π : ιType u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} {f' : (i : ι) → π i} {g' : (i : ι) → π i} [(i : ι) → Preorder (π i)] (hf : f Set.Icc f' g') (hg : g Set.Icc f' g') :
s.piecewise f g Set.Icc f' g'
theorem Finset.piecewise_mem_Icc {ι : Type u_1} (s : ) [(j : ι) → Decidable (j s)] {π : ιType u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} [(i : ι) → Preorder (π i)] (h : f g) :
s.piecewise f g Set.Icc f g
theorem Finset.piecewise_mem_Icc' {ι : Type u_1} (s : ) [(j : ι) → Decidable (j s)] {π : ιType u_3} {f : (i : ι) → π i} {g : (i : ι) → π i} [(i : ι) → Preorder (π i)] (h : g f) :
s.piecewise f g Set.Icc g f