# Update a function on a set of values #

This file defines Function.updateFinset, the operation that updates a function on a (finite) set of values.

This is a very specific function used for MeasureTheory.marginal, and possibly not that useful for other purposes.

def Function.updateFinset {ι : Type u_1} {π : ιSort u_2} [] (x : (i : ι) → π i) (s : ) (y : (i : { x : ι // x s }) → π i) (i : ι) :
π i

updateFinset x s y is the vector x with the coordinates in s changed to the values of y.

Equations
• = if hi : i s then y i, hi else x i
Instances For
theorem Function.updateFinset_def {ι : Type u_1} {π : ιSort u_2} {x : (i : ι) → π i} [] {s : } {y : (i : { x : ι // x s }) → π i} :
= fun (i : ι) => if hi : i s then y i, hi else x i
@[simp]
theorem Function.updateFinset_empty {ι : Type u_1} {π : ιSort u_2} {x : (i : ι) → π i} [] {y : (i : { x : ι // x }) → π i} :
= x
theorem Function.updateFinset_singleton {ι : Type u_1} {π : ιSort u_2} {x : (i : ι) → π i} [] {i : ι} {y : (i_1 : { x : ι // x {i} }) → π i_1} :
= Function.update x i (y i, )
theorem Function.update_eq_updateFinset {ι : Type u_1} {π : ιSort u_2} {x : (i : ι) → π i} [] {i : ι} {y : π i} :
theorem Function.updateFinset_updateFinset {ι : Type u_1} {π : ιType u_2} {x : (i : ι) → π i} [] {s : } {t : } (hst : Disjoint s t) {y : (i : { x : ι // x s }) → π i} {z : (i : { x : ι // x t }) → π i} :
= Function.updateFinset x (s t) (() (y, z))