Axioms for the theory of proveit.linear_algebra.vector_sets

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)

%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

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:

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:

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:

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:

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

%end axioms

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