minor changes

Author: AdamJasonKern

Game/Levels/LinearIndependenceSpanWorld/Code.lean

@@ -18,6 +18,8 @@ if then else
 -/
 import Game.Levels.LinearIndependenceSpanWorld.Level08
 
+namespace LinearAlgebraGame
+
 World "LinearIndependenceSpanWorld"
 Level 9
 
@@ -136,6 +138,8 @@ NewTactic tauto left right «let» ite
 
 NewTheorem Set.subset_insert Finset.Subset.antisymm_iff Finset.sum_eq_sum_diff_singleton_add Finset.mem_union_right Finset.sum_add_distrib Set.subset_diff_singleton Set.diff_subset
 
+TheoremDoc LinearAlgebraGame.remove_redundant_span as "remove_redundant_span" in "Vector Spaces"
+
 Statement remove_redundant_span
   {S : Set V} {w : V} (hcomb : w ∈ span K V (S \ {w})) :
   span K V S = span K V (S \ {w}) := by

Game/Levels/LinearIndependenceSpanWorld/Level09.lean

@@ -1,4 +1,4 @@
-\section{ZeroScalarMultiplication}Add commentMore actions
+\section{ZeroScalarMultiplication}
 
 \begin{definition}
   \label{definition : VectorSpace}

blueprint/src/chapters/chapter1/sheet1.tex

@@ -0,0 +1,11 @@
+\chapter{LinearIndependenceSpan}
+
+\input{chapters/chapter2/sheet1}
+\input{chapters/chapter2/sheet2}
+\input{chapters/chapter2/sheet3}
+\input{chapters/chapter2/sheet4}
+\input{chapters/chapter2/sheet5}
+\input{chapters/chapter2/sheet6}
+\input{chapters/chapter2/sheet7}
+\input{chapters/chapter2/sheet8}
+\input{chapters/chapter2/sheet9}

blueprint/src/chapters/chapter2.tex

@@ -0,0 +1,16 @@
+\section{LinearCombinations}
+
+\begin{definition}
+  \label{definition : linear_combination}
+  \lean{LinearAlgebraGame.is_linear_combination}
+  \leanok
+  \exists (s : Finset V) (f : V → K), (↑s ⊆ S) ∧ (x = Finset.sum s (fun v \Rightarrow f v \bullet v))
+\end{definition}
+
+\begin{theorem}
+  \label{theorem : linear_combination_of_mem}
+  \lean{LinearAlgebraGame.linear_combination_of_mem}
+  \leanok
+  \uses{definition : linear_combination}
+  If v $\in$ S, then v is a linear combination of S: {S : Set V} {v : V} (hv : v ∈ S) : is_linear_combination K V S v
+\end{theorem}

blueprint/src/chapters/chapter2/sheet1.tex

@@ -0,0 +1,18 @@
+\section{IntroducingSpan}
+
+
+\begin{definition}
+  \label{definition : span}
+  \lean{LinearAlgebraGame.is_linear_combination}
+  \leanok
+  \uses{definition : linear_combination}
+  ${ x \in V | linear_combination K V S x }$
+\end{definition}
+
+\begin{theorem}
+  \label{theorem : mem_span_of_mem}
+  \lean{LinearAlgebraGame.mem_span_of_mem}
+  \leanok
+  \uses{definition : linear_combination}
+  If $v \in S$, then $v \in span K V S$: {S : Set V} {v : V} (hv : v ∈ S) : v ∈ span K V S
+\end{theorem}

blueprint/src/chapters/chapter2/sheet2.tex

@@ -0,0 +1 @@
+\section{MonotonicityOfSpan}

blueprint/src/chapters/chapter2/sheet3.tex

@@ -0,0 +1 @@
+\section{LinearIndependence}

blueprint/src/chapters/chapter2/sheet4.tex

@@ -0,0 +1 @@
+\section{LinearIndependenceOfSubsets}

blueprint/src/chapters/chapter2/sheet5.tex

@@ -0,0 +1 @@
+\section{SupersetsSpanTheWholeSpace}