src/HOL/Analysis/Linear_Algebra.thy
changeset 66297 d425bdf419f5
parent 66287 005a30862ed0
child 66420 bc0dab0e7b40
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Jul 26 16:07:45 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Jul 27 15:22:35 2017 +0100
     1.3 @@ -79,20 +79,27 @@
     1.4  lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S"
     1.5    by (metis hull_subset subset_eq)
     1.6  
     1.7 -lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
     1.8 +lemma hull_Un_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
     1.9    unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
    1.10  
    1.11 -lemma hull_union:
    1.12 +lemma hull_Un:
    1.13    assumes T: "\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)"
    1.14    shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
    1.15 -  apply rule
    1.16 -  apply (rule hull_mono)
    1.17 -  unfolding Un_subset_iff
    1.18 -  apply (metis hull_subset Un_upper1 Un_upper2 subset_trans)
    1.19 -  apply (rule hull_minimal)
    1.20 -  apply (metis hull_union_subset)
    1.21 -  apply (metis hull_in T)
    1.22 -  done
    1.23 +  apply (rule equalityI)
    1.24 +  apply (meson hull_mono hull_subset sup.mono)
    1.25 +  by (metis hull_Un_subset hull_hull hull_mono)
    1.26 +
    1.27 +lemma hull_Un_left: "P hull (S \<union> T) = P hull (P hull S \<union> T)"
    1.28 +  apply (rule equalityI)
    1.29 +   apply (simp add: Un_commute hull_mono hull_subset sup.coboundedI2)
    1.30 +  by (metis Un_subset_iff hull_hull hull_mono hull_subset)
    1.31 +
    1.32 +lemma hull_Un_right: "P hull (S \<union> T) = P hull (S \<union> P hull T)"
    1.33 +  by (metis hull_Un_left sup.commute)
    1.34 +
    1.35 +lemma hull_insert:
    1.36 +   "P hull (insert a S) = P hull (insert a (P hull S))"
    1.37 +  by (metis hull_Un_right insert_is_Un)
    1.38  
    1.39  lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> S hull (insert a s) = S hull s"
    1.40    unfolding hull_def by blast