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
```