Documentation

Mathlib.Data.Finset.Update

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} [DecidableEq ι] (x : (i : ι) → π i) (s : Finset ι) (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
Instances For
    theorem Function.updateFinset_def {ι : Type u_1} {π : ιSort u_2} {x : (i : ι) → π i} [DecidableEq ι] {s : Finset ι} {y : (i : { x : ι // x s }) → π i} :
    Function.updateFinset x s y = 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} [DecidableEq ι] {y : (i : { x : ι // x }) → π i} :
    theorem Function.updateFinset_singleton {ι : Type u_1} {π : ιSort u_2} {x : (i : ι) → π i} [DecidableEq ι] {i : ι} {y : (i_1 : { x : ι // x {i} }) → π i_1} :
    Function.updateFinset x {i} y = Function.update x i (y i, )
    theorem Function.update_eq_updateFinset {ι : Type u_1} {π : ιSort u_2} {x : (i : ι) → π i} [DecidableEq ι] {i : ι} {y : π i} :
    theorem Function.updateFinset_updateFinset {ι : Type u_1} {π : ιType u_2} {x : (i : ι) → π i} [DecidableEq ι] {s : Finset ι} {t : Finset ι} (hst : Disjoint s t) {y : (i : { x : ι // x s }) → π i} {z : (i : { x : ι // x t }) → π i} :