Theorems · Definition

Function.update

{α : Sort u} → {β : α → Sort v} → [DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a

Replacing the value of a function at a given point by a given value.

Defined in

Mathlib.Logic.Function.Basic

Cited by

502 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 10 definitions · uses no axioms

Assumes

DecidableEq