Theory Linear_dependence

theory Linear_dependence
imports Comments
begin

section{*Linear dependence*}

context vector_space
begin

text{*In this section we will present the definition of linearly dependent set and linearly independent set. First of all
we will introduce the definition of @{text linear_combination}.*}

text{*A linear combination is a finite sum of vectors of $V$ multiplicated by scalars. 
However, how can we specify the scalars?
In a linear combination each vector will be multiplicated by one specific scalar, so this scalar depends on the vector. 
For that reason, we introduce the notion of @{text "coefficients_function"}. *}

(*definition coefficients_function :: "('b => 'a) set" where "coefficients_function = {f. f ∈ carrier V -> carrier K}"*)

definition coefficients_function :: "'b set => ('b => 'a) set"
  where "coefficients_function X 
  = {f. f ∈ X -> carrier K ∧ (∀x. x∉X --> f x = \<zero>\<^bsub>K\<^esub>)}"

text{*The explanation of the definition of coefficients function is as follows: given any set of vectors $X$,
its coefficients functions will be every function which maps each of the vectors in $X$ to scalars in $\mathbb{K}$.
We impose an additional condition, in such a way that every element out of the set of vectors $X$ is mapped to a
distinguished element (in this case @{term "\<zero>\<^bsub>K\<^esub>"}) of $\mathbb{K}$.*}
text{*The first condition in the definition (@{term "f ∈ X -> carrier K"}) is clear. A coefficients function is a 
function which maps, as we have said before, the elements of a given set $X$ to their corresponding scalars in 
$\mathbb{K}$. The second condition (@{term "∀x. x∉X --> f x = \<zero>\<^bsub>K\<^esub>"}) requires further explanation: the reason to map
every element out of the set $X$ to a distinguished point is that this allows us to compare coefficients functions
through the extensional equality of functions (@{thm fun_eq_iff[no_vars]}). Thus, two coefficients function will be equal
whenever they map every vector of $X$ to the same scalar of $\mathbb{K}$ (this statement would not hold in the
absence of the second condition). *}

text{*Giving @{term f} a coefficients function and a certain @{term x} in @{term "carrier V"} then @{term "f x"}
(the scalar of the vector) will be in @{term "carrier K"}.*}
lemma fx_in_K: 
  assumes x_in_V: "x ∈ carrier V" 
  and cf_f: "f ∈ coefficients_function (carrier V)" 
  shows "f(x) ∈ carrier K"
  using assms unfolding coefficients_function_def by auto

text{*For every @{term "x ∈ carrier V"}, multiplication 
  between the scalar and the vector (@{term "f x · x"}) is in @{term "carrier V"}.*}
lemma fx_x_in_V: 
  assumes x_in_V: "x ∈ carrier V" 
  and cf_f: "f ∈ coefficients_function (carrier V)" 
  shows "f(x)·x ∈ carrier V" 
  using mult_closed[OF x_in_V fx_in_K[OF x_in_V cf_f]] .

text{*Now we are going to define a linear combination. In Halmos, next section is about linear combinations, 
  however we have to introduce now the definition because we will use it to define the linear dependence of a set.
  We will use the definition of sums over a finite set (\emph{finsum}) which already exists in the Isabelle library.
  Note that we are defining a @{text linear_combination} with two parameters: second is the set of elements of
  @{term V} and first is the coefficients function which assigns each vector to its scalar.*}

text{*Due to the definition of @{term "finsum_def"} we are only considering the case of a finite linear combination.
  The case of infinite linear combinations is undefined. 
  This is not a problem for us, because we will work with finite vector
  spaces and in our development we will only need linear combinations over finite sets. In addition, the sums in
  an infinite vector space are all finite because without additional structure the axioms of a vector space
  do not permit us to meaningfully speak about an infinite sum of vectors.*}

definition linear_combination :: "('b => 'a) => 'b set => 'b"
  where "linear_combination f X = finsum V (λy. f(y)·y) X"

text{*In order to define the notion of linear dependence of a set we need to demand that this set be finite and 
  a subset of the carrier. To abbreviate notation we will define these two premises as @{text good_set}.*}

definition good_set :: "'b set => bool"
  where "good_set X = (finite X ∧ X ⊆ carrier V )"

text{*Next two lemmas show both properties:*}

lemma good_set_finite: 
  assumes good_set_X: "good_set X" 
  shows "finite X"
  using good_set_X
  unfolding good_set_def by simp

lemma good_set_in_carrier: 
  assumes good_set_X: "good_set X" 
  shows "X ⊆ carrier V"
  using good_set_X
  unfolding good_set_def by simp

text{*Empty set is a @{text good_set}.*}
lemma [simp]: "good_set {}"
  unfolding good_set_def by simp

text{*Now, we can present the definition of linearly dependent set. A set will be dependent if there exists a 
  linear combination equal to zero in which not all scalars are zero.*}

definition linear_dependent :: "'b set => bool"
  where "linear_dependent X = (good_set X 
  ∧ (∃f. f∈ coefficients_function (carrier V) ∧ linear_combination f X = \<zero>\<^bsub>V\<^esub> 
  ∧ ¬(∀x ∈ X. f x = \<zero>\<^bsub>K\<^esub>)))"

text{*This definition is equivalent to the previous one:*}
definition linear_dependent_2 :: "'b set => bool"
  where "linear_dependent_2 X =
  (∃f. f ∈ coefficients_function (carrier V) ∧ good_set X 
  ∧ linear_combination f X = \<zero>\<^bsub>V\<^esub> ∧ ¬ (∀x ∈ X. f x = \<zero>\<^bsub>K\<^esub>))"

text{*Next lemma, which is in the library, proves that are equivalent*}

lemma "(∃f. X ∧ Y f) = (X ∧ (∃f. Y f))"
  using ex_simps (2) [of X Y] .

lemma linear_dependent_eq_def:
  shows "linear_dependent X = linear_dependent_2 X"
  unfolding linear_dependent_def
  unfolding linear_dependent_2_def by blast

text{*We introduce now the notion of a linearly independent set. We will prove later that linear dependence
and independence are complementary notions (every set will be either dependent or independent).*}
definition linear_independent :: "'b set => bool"
  where "linear_independent X =
  (good_set X 
  ∧ (∀f. (f∈ coefficients_function (carrier V) ∧ linear_combination f X = \<zero>\<^bsub>V\<^esub>) 
  --> (∀x ∈ X. f(x)=\<zero>\<^bsub>K\<^esub>)))"

text{*Next lemmas prove that if we have a linear (in)dependent set 
  hence we have a @{text good_set} (finite and in the carrier).*}
lemma l_ind_good_set: "linear_independent X ==> good_set X"
  unfolding linear_independent_def by simp

lemma l_dep_good_set: "linear_dependent X ==> good_set X"
  unfolding linear_dependent_def by simp

text{*The empty set is linearly independent.*}
lemma empty_set_is_linearly_independent [simp]: 
  shows "linear_independent {}"
  unfolding linear_independent_def 
  by simp

text{*We can prove that linear independence is the opposite of linear dependence. For that, we first prove that
  every set which is not linearly independent must be linearly dependent:*}
lemma not_independent_implies_dependent:
  assumes good_set: "good_set X" 
  shows "¬ linear_independent X ==> linear_dependent X"
proof (unfold linear_dependent_def)
  assume not_linear_independent: "¬ linear_independent X"
  from not_linear_independent obtain f 
    where f_in_coefficients: "f ∈ coefficients_function (carrier V)" 
    and sum_zero: "linear_combination f X = \<zero>\<^bsub>V\<^esub>" 
    and not_all_zero: "¬(∀x ∈ X. f(x)=\<zero>\<^bsub>K\<^esub>)" 
    unfolding linear_independent_def using good_set by best
  have " f ∈ coefficients_function (carrier V)  
    ∧ linear_combination f X = \<zero>\<^bsub>V\<^esub> ∧ ¬ (∀x∈X. f x = \<zero>)"
    using  f_in_coefficients and good_set and sum_zero and not_all_zero 
    by simp
  hence "∃f. f ∈ coefficients_function (carrier V) 
    ∧ linear_combination f X = \<zero>\<^bsub>V\<^esub> ∧ ¬ (∀x∈X. f x = \<zero>)"
    by (rule exI [of _ "f"])
  thus "good_set X ∧ (∃f. f ∈ coefficients_function (carrier V) 
    ∧ linear_combination f X = \<zero>\<^bsub>V\<^esub> ∧ ¬ (∀x∈X. f x = \<zero>))"
    using good_set by simp
qed
text{*Now we prove that every set which is linearly dependent is not linearly independent:*}
lemma dependent_implies_not_independent: 
  shows "linear_dependent X ==> ¬ linear_independent X"
proof (rule impE)
  assume ld: "linear_dependent X"
  show "¬ linear_independent X"
  proof (unfold linear_independent_def)
    from ld obtain f where good_set: "good_set X" 
      and cf_f: "f ∈ coefficients_function (carrier V)" 
      and lc_f_X_zero: "linear_combination f X = \<zero>\<^bsub>V\<^esub> "
      and not_all_zero: " ¬(∀x ∈ X. f x = \<zero>\<^bsub>K\<^esub>)" 
      unfolding linear_dependent_def by auto
    have "¬ (∀f. f ∈ coefficients_function (carrier V)  
      ∧ linear_combination f X = \<zero>\<^bsub>V\<^esub> --> (∀x∈X. f x = \<zero>))" 
      using cf_f and lc_f_X_zero and not_all_zero by auto
    thus " ¬ (good_set X 
      ∧ (∀f. f ∈ coefficients_function (carrier V)  
      ∧ linear_combination f X = \<zero>\<^bsub>V\<^esub> --> (∀x∈X. f x = \<zero>)))"
      using good_set by auto
  qed
qed (auto)

text{*Hence the result:*}
lemma dependent_if_only_if_not_independent:
  assumes good_set: "good_set X"
  shows "linear_dependent X <-> ¬ linear_independent X"
  using dependent_implies_not_independent 
    and not_independent_implies_dependent [OF good_set] by auto

text{*Analogously, we can prove that a set is not linearly dependent if and only if it is linearly independent. 
  We use @{thm swap[no_vars]} and the previous lemma:*}

lemma not_dependent_implies_independent: 
  assumes good_set: "good_set X" 
  shows "¬ linear_dependent X ==> linear_independent X"
proof -
  assume not_linear_dependent: "¬ linear_dependent X"
  have imp: "¬ linear_independent X ==> linear_dependent X" 
    using not_independent_implies_dependent [OF good_set] .
  show "linear_independent X"
    apply (rule swap [OF not_linear_dependent imp]) .
qed

lemma independent_implies_not_dependent: 
  shows "linear_independent X ==> ¬ linear_dependent X"
proof -
  assume li: "linear_independent X"
  have imp: "linear_dependent X ==> ¬ linear_independent X" 
    using dependent_implies_not_independent .
  show "¬ linear_dependent X" apply (rule swap[OF _ imp]) 
    using li by simp+
qed

text{*Finally, we obtain the equivalence of definitions:*}
lemma independent_if_only_if_not_dependent:
  assumes good_set: "good_set X"
  shows "linear_independent X <-> ¬ linear_dependent X"
  using independent_implies_not_dependent 
    and not_dependent_implies_independent [OF good_set]
  by fast

text{*Every good set will be either dependent or independent (but not both at the same time). 
  Note: the operator OR of this proof is not an exclusive OR, so
  really here we are proving that every set is either dependent or independent or both.*}
lemma li_or_ld: 
  assumes good_set:"good_set X" 
  shows "linear_dependent X | linear_independent X"  
proof (cases "linear_dependent X")
  case False show ?thesis
    using not_dependent_implies_independent [OF good_set] by fast
next
  case True thus ?thesis by fast
qed

text{*In order to avoid that problem, we need to implement the operator exclusive OR:*}

definition xor :: "bool => bool => bool"
  where "xor A B ≡ (A ∧ ¬ B) ∨ (¬A ∧ B)"

text{*Now we can prove that every good set will be either dependent or independent (but not both at the same time):*}
lemma li_xor_ld: 
  assumes good_set:"good_set X" 
  shows "xor (linear_dependent X) (linear_independent X)"  
proof (unfold xor_def,auto)
  assume ld_X: "linear_dependent X" 
    and li_X: "linear_independent X"
  have "¬ linear_independent X" 
    using dependent_implies_not_independent[OF ld_X] .
  thus False using li_X by contradiction
next
  assume "¬ linear_independent X" thus "linear_dependent X"
    using not_independent_implies_dependent[OF good_set _] 
    by simp
qed


text{*A corollary of these theorems using that the empty set is linearly independent:
  if we have a linearly dependent set, then it isn't the empty set:*}
lemma dependent_not_empty: 
  assumes ld_A: "linear_dependent A" 
  shows "A≠{}"
 using dependent_implies_not_independent[OF ld_A] empty_set_is_linearly_independent by auto

text{*Now we prove that every set $X$ containing a linearly dependent subset $Y$ is itself linearly dependent.
This property is stated in Halmos but not proved, he says that the fact is clear.*}

text{*The proof is easy but long. We want to achieve a linear combination of the elements of $X$ equal to zero
  and where not all scalars are zero. We know that a subset $Y$ of $X$ is dependent, so there exists a linear combination
  of the elements of $Y$ equal to zero where not all scalars are zero (we will denote its coefficients funcion as $f$). 
  If we define a coefficients function for the set $X$ where the scalars of the elements $y \in Y$ are $f(y)$ and $0_K$
  for the rest of elements in $X$, then we will obtain a linear combination of elements of $X$ equal to zero where
not all scalars are zero (because not for all $x \in Y$ $f(x)$ is $0_K$).*}
lemma linear_dependent_subset_implies_linear_dependent_set:
  assumes Y_subset_X: "Y ⊆ X" and good_set: "good_set X"
  and linear_dependent_Y: "linear_dependent Y"
  shows "linear_dependent X"
proof (unfold linear_dependent_def)
    --"Using that Y is dependent, we can obtain a linear combination equal to zero where not all scalars are zero."
  from linear_dependent_Y 
  obtain f where sum_zero_f_Y:"linear_combination f Y = \<zero>\<^bsub>V\<^esub>" 
    and not_all_zero_f:" ¬ (∀x∈Y. f x = \<zero>)"
    and coefficients_function_f:
    "f ∈ coefficients_function (carrier V) " 
    unfolding linear_dependent_def 
    by best
      --"Now we define the function and prove that is a coefficients function:"
  let ?g= "(λx. if x ∈ Y then f(x) else \<zero>\<^bsub>K\<^esub>)"
  have coefficients_function_g: 
    "?g ∈ coefficients_function (carrier V) "
    using coefficients_function_f
    unfolding coefficients_function_def 
    by auto
      -- "We want to prove another two things: that the linear combination is zero and
      not all scalars are zero."
      --"First:"
  have sum_zero_g_X: "linear_combination ?g X = \<zero>\<^bsub>V\<^esub>"
  proof -
      --"We will separate the linear combination into two ones, in the set $Y$ and in the set $X-Y$. We can do it
      thanks to the theorem @{text finsum_Un_disjoint}: @{thm finsum_Un_disjoint[no_vars]} and 
      that the descomposition of the sets is disjoint."
      --"Some properties which we will need for the proof:"
    have descomposicion_conjuntos:"X=Y∪(X-Y)"
      using Y_subset_X by auto 
    have disjuntos: "Y ∩ (X-Y)={}" 
      by simp
    have finite_X: "finite X" 
      using good_set 
      unfolding good_set_def by simp
    have finite_Y: "finite Y"
      using linear_dependent_Y 
      unfolding linear_dependent_def 
      unfolding good_set_def by auto
    have finite_X_minus_Y: "finite (X-Y)" 
      using finite_X  by simp
    have g1:"?g ∈ Y -> carrier K" 
      using coefficients_function_g 
      unfolding coefficients_function_def 
      using good_set 
      unfolding good_set_def 
      using Y_subset_X
      by auto
    have g2:"?g ∈ (X-Y) -> carrier K" 
      using coefficients_function_g 
      unfolding coefficients_function_def 
      using good_set 
      unfolding good_set_def 
      by auto
    let ?h="(λx. ?g(x)·x)"
    have h1: "?h ∈ Y -> carrier V"
    proof
      fix x
      assume x_in_Y: "x∈Y"
      have x_in_V: "x∈ carrier V"
      proof
        have Y_subset_V: "Y⊆ carrier V"
          using good_set
          unfolding good_set_def
          using Y_subset_X
          by auto
        show ?thesis using Y_subset_V and x_in_Y by auto
      qed (auto)
      have gx_in_K: "?g(x)∈ carrier K"
        using g1
        using x_in_Y 
        unfolding Pi_def by auto
      have gx_x_in_V: "?g(x)·x ∈ carrier V"
        using mult_closed [OF x_in_V gx_in_K] by auto 
      show "(if x ∈ Y then f x else \<zero>) · x ∈ carrier V" 
        using gx_x_in_V by auto
    qed
    have h2: "?h ∈ (X-Y) -> carrier V"
    proof
      fix x
      assume x_in_X_minus_Y: "x∈ (X-Y)"
      have x_in_V: "x∈ carrier V"
      proof
        have X_minus_Y_subset_V: "(X-Y) ⊆ carrier V"
          using good_set
          unfolding good_set_def
          using Y_subset_X
          by auto
        show ?thesis
          using X_minus_Y_subset_V
          using x_in_X_minus_Y by auto
      qed (auto)
      have gx_in_K: "?g(x)∈ carrier K"         
        using x_in_X_minus_Y 
        by auto
      have gx_x_in_V: "?g(x)·x ∈ carrier V" 
        using mult_closed [OF x_in_V gx_in_K] by auto 
      show "(if x ∈ Y then f x else \<zero>) · x ∈ carrier V" 
        using gx_x_in_V by auto
    qed
        --"And now the decomposition. We will make a calculation until we achieve the thesis."
    have "linear_combination ?g X 
      = linear_combination ?g (Y∪(X-Y))" 
      using descomposicion_conjuntos by simp
    also have descomposicion: 
      "...=linear_combination ?g Y ⊕\<^bsub>V\<^esub> linear_combination ?g (X-Y)" 
      unfolding linear_combination_def 
      using finsum_Un_disjoint [OF finite_Y finite_X_minus_Y 
        disjuntos h1 h2]
      by auto
        --"First linear combination of right term is the same linear combination of the elements of Y where it was equal 
        to zero."
    also have "...=\<zero>\<^bsub>V\<^esub> ⊕\<^bsub>V\<^esub> linear_combination ?g (X-Y)"
    proof -
      have "linear_combination ?g Y=linear_combination f Y"
      proof (unfold linear_combination_def)
        have iguales: "Y=Y" ..
        show "(\<Oplus>\<^bsub>V\<^esub>y∈Y. (if y ∈ Y then f y else \<zero>) · y) 
          = (\<Oplus>\<^bsub>V\<^esub>y∈Y. f y · y)"
          using finsum_cong [OF iguales] using h1 by auto
      qed
      also have "...=\<zero>\<^bsub>V\<^esub>" using sum_zero_f_Y .
      finally show ?thesis by simp
    qed
    also have "...=\<zero>\<^bsub>V\<^esub> ⊕\<^bsub>V\<^esub> \<zero>\<^bsub>V\<^esub>"
    proof -
        --"Thanks to the definition of ?g, the linear combination in $(X-Y)$ is also zero (because all scalars are zero)."
        --"As each scalar is zero, the multiplication between it and its vector is zero (@{text zeroK_mult_V_is_zeroV}:
        @{thm zeroK_mult_V_is_zeroV[no_vars]}).
        Then we are adding a finite sum of zeros, so it will be zero 
        using @{text finsum_zero}: @{thm finsum_zero[no_vars]}."
      have sum_g_X_minus_Y:"linear_combination ?g (X-Y)=\<zero>\<^bsub>V\<^esub>"
      proof -
        have X_subset_V: "X ⊆ carrier V" 
          using good_set 
          unfolding good_set_def by auto
        hence X_minus_Y_subset_V:"(X-Y) ⊆ carrier V"  by auto
        have not_in_Y: "x∈ (X-Y)==> x∉ Y" by auto
        have "linear_combination ?g (X-Y)=(\<Oplus>\<^bsub>V\<^esub>y∈X - Y.  \<zero> · y)" 
        proof (unfold linear_combination_def)
          have igualesX_minus_Y: "X-Y=X-Y"..
          show "(\<Oplus>\<^bsub>V\<^esub>y∈X - Y. (if y ∈ Y then f y else \<zero>) · y) 
            = finsum V (op · \<zero>) (X - Y)"
            using finsum_cong [OF igualesX_minus_Y eqTrueI [OF h2]] 
            by auto
        qed
        also have "…=(\<Oplus>\<^bsub>V\<^esub>y∈X - Y. \<zero>\<^bsub>V\<^esub>)"      
        proof (rule finsum_cong')
          show "X - Y = X - Y" ..
          show "(λy. \<zero>\<^bsub>V\<^esub>) ∈ X - Y -> carrier V" by simp
          show "!!i. i ∈ X - Y ==> \<zero> · i = \<zero>\<^bsub>V\<^esub>"
            using zeroK_mult_V_is_zeroV
            using X_minus_Y_subset_V by auto
        qed  
        also have "…=\<zero>\<^bsub>V\<^esub>"
          using finsum_zero [OF finite_X_minus_Y] .
        finally show ?thesis .
      qed
      thus ?thesis by simp
    qed
    also have "...=\<zero>\<^bsub>V\<^esub>" by simp
    finally show ?thesis .
  qed
      --"Second property is easy:"
  have not_all_zero_g: "¬ (∀x∈X. ?g x = \<zero>)" 
    using Y_subset_X 
    using not_all_zero_f by auto
  have "?g ∈ coefficients_function (carrier V)  
    ∧ linear_combination ?g X = \<zero>\<^bsub>V\<^esub> ∧ ¬ (∀x∈X. ?g x = \<zero>)"
    using coefficients_function_g and good_set 
      and sum_zero_g_X and not_all_zero_g by fast
  hence
    "∃f. f ∈ coefficients_function (carrier V)  
    ∧ linear_combination f X = \<zero>\<^bsub>V\<^esub> ∧ ¬ (∀x∈X. f x = \<zero>)"
    by (rule exI[of _ ?g])
  thus "good_set X ∧ (∃f. f ∈ coefficients_function (carrier V) 
    ∧ linear_combination f X = \<zero>\<^bsub>V\<^esub> ∧ ¬ (∀x∈X. f x = \<zero>))" 
    using good_set by simp
qed


text{*More properties and facts: *}
lemma exists_subset_ld:
  assumes ld_X: "linear_dependent X" 
  shows "∃Y. Y ⊆ X ∧ linear_dependent Y"
  using ld_X by auto

lemma exists_subset_li: 
  assumes ld_X: "linear_dependent X" 
  shows "∃Y. Y⊆X ∧ linear_independent Y"
proof (rule exI[of _ "{}"])
  show "{}⊆X ∧ linear_independent {}" 
    using empty_set_is_linearly_independent by auto
qed

text{*A set containing @{term "\<zero>\<^bsub>V\<^esub>"} is not an independent set:*}
lemma zero_not_in_linear_independent_set: 
  assumes li_A: "linear_independent A"
  shows "\<zero>\<^bsub>V\<^esub> ∉ A"
proof (cases "\<zero>\<^bsub>V\<^esub> ∉ A")
  case True thus ?thesis .
next
  case False show ?thesis
  proof -
    have cb_A: "good_set A" using l_ind_good_set[OF li_A] .
    have zero_in_A: "\<zero>\<^bsub>V\<^esub> ∈ A" using False by simp
    let ?g="(λx. if x=\<zero>\<^bsub>V\<^esub> then \<one>\<^bsub>K\<^esub> else \<zero>\<^bsub>K\<^esub>)"
    have cf_g: "?g ∈ coefficients_function (carrier V)" 
      unfolding coefficients_function_def by auto
    have lc_zero: "linear_combination ?g A=\<zero>\<^bsub>V\<^esub>"
    proof (unfold linear_combination_def)
      have "(\<Oplus>\<^bsub>V\<^esub>y∈A. (if y = \<zero>\<^bsub>V\<^esub> then \<one> else \<zero>) · y)
        =(\<Oplus>\<^bsub>V\<^esub>y∈A. \<zero>\<^bsub>V\<^esub>)"
      proof (rule finsum_cong',auto)
        show "\<one> · \<zero>\<^bsub>V\<^esub> = \<zero>\<^bsub>V\<^esub>" 
          using scalar_mult_zeroV_is_zeroV by auto
        fix i
        assume i_in_A: "i ∈ A" and i_not_zero: "i ≠ \<zero>\<^bsub>V\<^esub>"
        show "\<zero> · i = \<zero>\<^bsub>V\<^esub>" 
          using zeroK_mult_V_is_zeroV and i_in_A and cb_A 
          unfolding good_set_def by auto
      qed
      also have "...=\<zero>\<^bsub>V\<^esub>" 
        using finsum_zero using good_set_finite[OF cb_A] by auto
      finally show 
        "(\<Oplus>\<^bsub>V\<^esub>y∈A. (if y = \<zero>\<^bsub>V\<^esub> then \<one> else \<zero>) · y) = \<zero>\<^bsub>V\<^esub>" .
    qed
    have not_all_zero: "¬(∀x∈A. ?g x = \<zero>)" 
      using zero_in_A by auto 
      --"Contradiction with @{text linear_independent}"
    show ?thesis 
      using cf_g lc_zero not_all_zero li_A 
      unfolding linear_independent_def by auto
  qed 
qed

text{*Every subset of an independent set is also independent. 
  This property has been proved using \emph{sledgehammer}.*}
lemma independent_set_implies_independent_subset:
  assumes A_in_B: "A ⊆ B"
  and li_B: "linear_independent B"
  shows "linear_independent A"
  by (metis A_in_B good_set_def good_set_finite good_set_in_carrier
    dependent_implies_not_independent finite_subset l_ind_good_set
    li_B linear_dependent_subset_implies_linear_dependent_set
    not_independent_implies_dependent subset_trans)

text{*We can even extend the notions of linearly dependent and independent sets to infinite sets in the following way.
We shall say that a set is linearly independent if every finite subset of it is such.*}
definition linear_independent_ext:: "'b set => bool"
  where "linear_independent_ext X 
  = (∀A. finite A ∧ A ⊆ X --> linear_independent A)"

text{*Otherwise, it is linearly dependent.*}
definition linear_dependent_ext:: "'b set => bool"
  where "linear_dependent_ext X 
  = (∃A. A ⊆ X ∧ linear_dependent A)"


text{*As expected, if we have a linearly independent set it will be also 
  @{text linear_independent_ext} set.*}
lemma independent_imp_independent_ext:
  assumes li_X: "linear_independent X"
  shows "linear_independent_ext X"
proof -
  have fin_X: "finite X" and X_in_V: "X ⊆ carrier V"
    using l_ind_good_set[OF li_X] unfolding good_set_def by simp+
  show ?thesis unfolding linear_independent_ext_def
  proof (auto)
    fix A
    assume A_in_X: "A ⊆ X"
    show "linear_independent A"
      using independent_set_implies_independent_subset
      [OF A_in_X li_X] .
  qed
qed

text{*The same property holds for dependent sets:*}
lemma dependent_imp_dependent_ext:
  assumes ld_X: "linear_dependent X"
  shows "linear_dependent_ext X"
  unfolding linear_dependent_ext_def 
  using l_dep_good_set[OF ld_X] 
  unfolding good_set_def 
  using ld_X 
  by fast


text{*Every finite set which is @{text linear_independent_ext} will also be @{text linear_independent}:*}
lemma fin_ind_ext_impl_ind:
  assumes li_ext_X: "linear_independent_ext X"
  and finite_X: "finite X"
  shows "linear_independent X"
  by (metis finite_X li_ext_X linear_independent_ext_def subset_refl)

text{*Similarly with the notion of linear dependence:*}
lemma fin_dep_ext_impl_dep:
  assumes ld_ext_X: "linear_dependent_ext X"
  and gs_X: "good_set X"
  shows "linear_dependent X" 
  by (metis gs_X ld_ext_X linear_dependent_ext_def 
    linear_dependent_subset_implies_linear_dependent_set)


text{*We can prove that also in the infinite case, the definitions of @{text linear_independent_ext}
and @{text linear_dependent_ext} are complementary (every set will be of one type or the other). Let's see it:*}

lemma not_independent_ext_implies_dependent_ext:
  assumes X_in_V: "X ⊆ carrier V"
  shows "¬ linear_independent_ext X ==> linear_dependent_ext X"
  unfolding linear_independent_ext_def and linear_dependent_ext_def 
  using not_independent_implies_dependent and X_in_V 
  unfolding good_set_def 
  by auto

lemma not_dependent_ext_implies_independent_ext:
  assumes X_in_V: "X ⊆ carrier V"
  shows "¬ linear_dependent_ext X ==> linear_independent_ext X"
  by (metis X_in_V not_independent_ext_implies_dependent_ext)

lemma independent_ext_implies_not_dependent_ext:
  shows "linear_independent_ext X ==> ¬ linear_dependent_ext X"
  by (metis good_set_finite independent_implies_not_dependent 
    l_dep_good_set linear_dependent_ext_def 
    linear_independent_ext_def)

lemma dependent_ext_implies_not_independent_ext:
  shows "linear_dependent_ext X ==> ¬ linear_independent_ext X"
  by (metis independent_ext_implies_not_dependent_ext)

corollary dependent_ext_if_only_if_not_indepentent_ext:
  assumes X_in_V: "X ⊆ carrier V"
  shows "linear_dependent_ext X <-> ¬ linear_independent_ext X"
  using assms not_independent_ext_implies_dependent_ext 
    dependent_ext_implies_not_independent_ext
  by blast  

corollary independent_ext_if_only_if_not_depentent_ext:
  assumes X_in_V: "X ⊆ carrier V"
  shows "linear_independent_ext X <-> ¬ linear_dependent_ext X"
  using assms not_dependent_ext_implies_independent_ext 
    independent_ext_implies_not_dependent_ext
  by blast  

end
end