logo

Theorems (or conjectures) for the theory of proveit.linear_algebra.linear_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 Function
from proveit import x, y, K, P, V, W
from proveit.logic import Forall, InSet, InClass, Equals
from proveit.linear_algebra import (
    VecSpaces, LinMap, VecAdd, LinMapAdd)
In [2]:
%begin theorems
Defining theorems for theory 'proveit.linear_algebra.linear_maps'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

A linear map from $V$ to $W$ will map an element of $V$ to an element of $W$. We don't place a restriction on $V$ or $W$, but they should be proper vector spaces for $P \in \mathcal{L}(V, W)$ to be provable.

In [3]:
lin_map_domains = Forall(
    (V, W), Forall(P, Forall(x, InSet(Function(P, x), W),
                             domain=V),
                   domain=LinMap(V, W)))
Out[3]:
lin_map_domains (conjecture without proof):

In [4]:
lin_map_linearity = Forall(
    (V, W), Forall(P, Forall((x, y), 
                             Equals(Function(P, VecAdd(x, y)),
                                    VecAdd(Function(P, x),
                                           Function(P, y))),
                             domain=V),
                   domain=LinMap(V, W)))
Out[4]:
lin_map_linearity (conjecture without proof):

Linear map sets are vector spaces

In [5]:
lin_map_is_vec_space = Forall(
    K, Forall(
        (V, W), InClass(LinMap(V, W), VecSpaces(K)),
        domain=VecSpaces(K)))
Out[5]:
lin_map_is_vec_space (conjecture without proof):

In [6]:
%end theorems
These theorems may now be imported from the theory package: proveit.linear_algebra.linear_maps