Theorems · Theorem

Function.update_apply

∀ {α : Sort u} [inst : DecidableEq α] {β : Sort u_1} (f : α → β) (a' : α) (b : β) (a : α),
  Function.update f a' b a = if a = a' then b else f a

On non-dependent functions, Function.update can be expressed as an ite

Defined in

Mathlib.Logic.Function.Basic

Cited by

23 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext

Assumes

DecidableEq