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

• Function.updateFinset x s y i = if hi : i ∈ s then y { val := i, property := hi } else x i

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 { val := i, property := hi } else x i

@[simp]

theorem Function.updateFinset_empty {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] {y : (i : { x : ι // x ∈ ∅ }) → π ↑i} : Function.updateFinset x ∅ y = x

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 { val := i, property := ⋯ })

theorem Function.update_eq_updateFinset {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [DecidableEq ι] {i : ι} {y : π i} : Function.update x i y = Function.updateFinset x {i} (uniqueElim y)

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} : Function.updateFinset (Function.updateFinset x s y) t z = Function.updateFinset x (s ∪ t) ((Equiv.piFinsetUnion π hst) (y, z))