Update for finite functions

This module defines the update operation for finite functions, that is, the equivalent of Function.update for FinFun.

def Cslib.FinFun.update {β : Type u_1} {α : Type u_2} [Zero β] [DecidableEq α] [DecidableEqZero β] (f : FinFun α β) (a : α) (b : β) : FinFun α β

FinFun equivalent of Function.update.

Equations

• f.update a b = { fn := Function.update f.fn a b, support := if b = 0 then f.support \ {a} else f.support ∪ {a}, mem_support_fn := ⋯ }

@[simp]

theorem Cslib.FinFun.update_coe {β : Type u_2} {α : Type u_1} [Zero β] [DecidableEq α] [DecidableEqZero β] {a : α} {b : β} (f : FinFun α β) : ⇑(f.update a b) = Function.update (⇑f) a b

FinFun.update is consistent with Function.update.

theorem Cslib.FinFun.update_apply {β : Type u_2} {α : Type u_1} [Zero β] [DecidableEq α] [DecidableEqZero β] {a' : α} {b : β} {a : α} (f : FinFun α β) : (f.update a' b) a = if a = a' then b else f a

Conditional characterisation of the functional interface of FinFun.update.

theorem Cslib.FinFun.update_support {β : Type u_2} {α : Type u_1} [Zero β] [DecidableEq α] [DecidableEqZero β] {a : α} {b : β} (f : FinFun α β) : (f.update a b).support = if b = 0 then f.support \ {a} else f.support ∪ {a}

Conditional characterisation of the support of an updated FinFun.

@[simp]

theorem Cslib.FinFun.update_idem {β : Type u_2} {α : Type u_1} [Zero β] [DecidableEq α] [DecidableEqZero β] {a : α} {b b' : β} (f : FinFun α β) : (f.update a b).update a b' = f.update a b'

Updating a finite function on the same key is the same as doing the last update.

theorem Cslib.FinFun.update_comm {β : Type u_2} {α : Type u_1} [Zero β] [DecidableEq α] [DecidableEqZero β] {a a' : α} {b b' : β} (f : FinFun α β) (h : a ≠ a') : (f.update a b).update a' b' = (f.update a' b').update a b

Updates on different keys commute.

theorem Cslib.FinFun.update_self {β : Type u_2} {α : Type u_1} [Zero β] [DecidableEq α] [DecidableEqZero β] {a : α} (f : FinFun α β) : f.update a (f a) = f

Updates that do not change mappings are redundant.

theorem Cslib.FinFun.update_support_subseteq {β : Type u_2} {α : Type u_1} [Zero β] [DecidableEq α] [DecidableEqZero β] {a : α} {b : β} (f : FinFun α β) : (f.update a b).support ⊆ f.support ∪ {a}

Updating a function never grows its support more than adding the key.