logo

Axioms for the theory of proveit.linear_algebra.linear_maps

In [1]:
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.

from proveit import Function, Lambda, Conditional
from proveit import c, x, A, B, P, V, W
from proveit.logic import Forall, Equals, InSet
from proveit.linear_algebra import (
    VecSpaces, LinMap, VecAdd, ScalarMult)
In [2]:
%begin axioms

Defining axioms for theory 'proveit.linear_algebra.linear_maps'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions
In [ ]:
In [ ]:

Define vector addition and scalar multiplication on LinMaps

In [3]:
vec_add_lin_map = Forall(
    (V, W), Forall(
        (A, B), Equals(VecAdd(A, B),
                       Lambda(x, Conditional(
                           VecAdd(Function(A, x), 
                                  Function(B, x)),
                           InSet(x, V)))),
        domain=LinMap(V, W)))
Out[3]:
vec_add_lin_map:
In [4]:
scalar_mult_lin_map = Forall(
    (V, W), Forall(
        (c, P), Equals(ScalarMult(c, P),
                       Lambda(x, Conditional(
                           ScalarMult(c, Function(P, x)),
                           InSet(x, V)))),
        domain=LinMap(V, W)))
Out[4]:
scalar_mult_lin_map:
In [5]:
%end axioms

These axioms may now be imported from the theory package: proveit.linear_algebra.linear_maps