Theorems · Theorem

Function.update_self

∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (a : α) (v : β a) (f : (a : α) → β a),
  Function.update f a v a = v

Defined in

Mathlib.Logic.Function.Basic

Cited by

201 results in Mathlib

Foundations

Depth 7 from the axioms, rests on 12 definitions · uses no axioms

Assumes

DecidableEq