Theorems (or conjectures) for the theory of proveit.linear_algebra.linear_maps

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, Lambda, Conditional
from proveit import c, x, y, A, B, K, P, V, W
from proveit.logic import Forall, InSet, InClass, Equals
from proveit.linear_algebra import (
    VecSpaces, VecAdd, ScalarMult, LinMap, LinMapAdd, Identity)

%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.

lin_map_domains = Forall(
    (V, W), Forall(P, Forall(x, InSet(Function(P, x), W),
                             domain=V),
                   domain=LinMap(V, W)))

lin_map_domains (conjecture without proof):

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

lin_map_linearity (conjecture without proof):

Forall(V, InSet(Identity(V), LinMap(V, V)))

Linear map sets are vector spaces

lin_map_is_vec_space = Forall(
    K, Forall(
        (V, W), InClass(LinMap(V, W), VecSpaces(K)),
        domain=VecSpaces(K)))

lin_map_is_vec_space (conjecture without proof):

%end theorems

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