# 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 (

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),
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