# Theorems (or conjectures) for the theory of proveit.core_expr_types.lambda_maps¶

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import Conditional, Lambda
from proveit import i, a, b, c, f, g, Q
from proveit.core_expr_types import (
a_1_to_i, b_1_to_i, c_1_to_i,
f__a_1_to_i, g__a_1_to_i, f__b_1_to_i, g__c_1_to_i,
Q__a_1_to_i, Q__b_1_to_i, Q__c_1_to_i)
from proveit.logic import Forall, Implies, Equals
from proveit.numbers import NaturalPos

In [2]:
%begin theorems

Defining theorems for theory 'proveit.core_expr_types.lambda_maps'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

In [3]:
general_lambda_substitution = \
Forall(i, Forall((f, g, Q),
Implies(Forall(a_1_to_i,
Equals(f__a_1_to_i,
g__a_1_to_i),
conditions = [Q__a_1_to_i]),
Equals(Lambda(b_1_to_i,
Conditional(f__b_1_to_i,
Q__b_1_to_i)),
Lambda(c_1_to_i,
Conditional(g__c_1_to_i,
Q__c_1_to_i))) \
.with_wrap_after_operator()).with_wrap_after_operator()),
domain=NaturalPos)

general_lambda_substitution (conjecture without proof):

In [4]:
%end theorems

These theorems may now be imported from the theory package: proveit.core_expr_types.lambda_maps