Lambda Function x ↦ A

(lambda x A) represents a function that maps the input x to the value A. (lambda x (+ (* (3) x) (4))) is a function (apply f x) that takes x as the input and returns (= (apply f x) (+ (* (3) x) (4))).

The lambda function is defined as (=_ (lambda y A) ({|} x (E. y (= x (<,> y A))))) /edit/peano/peano_thms.gh/df-lambda.

Theorems

How to find the value of the lambda function for a particular input (function application)

Functions Overview

Login to edit