# Axioms for the theory of proveit.linear_algebra.vector_sets¶

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 n, v, w, K, H, V
from proveit.core_expr_types import a_1_to_n, x_1_to_n
from proveit.logic import And, Forall, Exists, Equals, Set, InSet, NotInSet, SetOfAll
from proveit.numbers import NaturalPos, Complex, KroneckerDelta
from proveit.linear_algebra import lin_comb_axn, some_nonzero_a
from proveit.linear_algebra import (
VecSpaces, VecZero, InnerProd, InnerProdSpaces,
SpanningSets, LinDepSets, Bases, Span, Dim)

In [2]:
%begin axioms

Defining axioms for theory 'proveit.linear_algebra.vector_sets'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

In [3]:
span_def = Forall(K, Forall(
V, Forall(
n, Forall(x_1_to_n,
Equals(Span(Set(x_1_to_n)),
SetOfAll(a_1_to_n, lin_comb_axn,
domain=K)).with_wrap_after_operator(),
domain=V).with_wrapping(),
domain=NaturalPos),
domain=VecSpaces(K)))

span_def:
In [4]:
spanning_set_def = Forall(K, Forall(
V, Forall(
n, Forall((x_1_to_n),
Equals(InSet(Set(x_1_to_n), SpanningSets(V)),
Equals(V, Span(Set(x_1_to_n)))),
domain=V).with_wrapping(),
domain=NaturalPos),
domain=VecSpaces(K)))

spanning_set_def:
In [5]:
lindep_set_def = Forall(K, Forall(
V, Forall(
n, Forall((x_1_to_n),
Equals(InSet(Set(x_1_to_n), LinDepSets(V)),
Exists(a_1_to_n,
Equals(lin_comb_axn, VecZero(V)),
domain=K,
condition=some_nonzero_a)
.with_wrapping())
.with_wrap_after_operator(),
domain=V).with_wrapping(),
domain=NaturalPos),
domain=VecSpaces(K)))

lindep_set_def:
In [6]:
bases_def = Forall(K, Forall(
V, Forall(
n, Forall(x_1_to_n,
Equals(InSet(Set(x_1_to_n), Bases(V)),
And(InSet(Set(x_1_to_n), SpanningSets(V)),
NotInSet(Set(x_1_to_n), LinDepSets(V)))
.with_wrap_after_operator())
.with_wrap_after_operator(),
domain=V).with_wrapping(),
domain=NaturalPos),
domain=VecSpaces(K)))

bases_def:
In [7]:
# Every basis of a finite basis set has the same number of vectors,
# so we define Dim(V) as the number of vectors in any basis of V.
dim_def = Forall(K, Forall(
V, Forall(
n, Forall(x_1_to_n,
Equals(Dim(V), n),
condition=InSet(Set(x_1_to_n), Bases(V))),
domain=NaturalPos),
domain=VecSpaces(K)))

dim_def:
In [8]:
%end axioms

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