# [isabelle] Weak lemmas in HOL-Analysis.Affine

```Dear Isabelle maintainers,

(which mailinglist should this go on? I'm not sure)

I have encountered some weak theorems in HOL-Analysis.Affine, where a
type is constrained to an euclidean space while any real vector space
suffices. Please consider the following diff.

Regards,
Jakub Kądziołka

@@ -1008,7 +1008,7 @@
using affine_hull_span_gen[of "0" S] assms by auto

lemma extend_to_affine_basis_nonempty:
-  fixes S V :: "'n::euclidean_space set"
+  fixes S V :: "'n::real_vector set"
assumes "\<not> affine_dependent S" "S \<subseteq> V" "S \<noteq> {}"
shows "\<exists>T. \<not> affine_dependent T \<and> S \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
proof -
@@ -1044,7 +1044,7 @@
qed

lemma affine_basis_exists:
-  fixes V :: "'n::euclidean_space set"
+  fixes V :: "'n::real_vector set"
shows "\<exists>B. B \<subseteq> V \<and> \<not> affine_dependent B \<and> affine hull V = affine hull B"
proof (cases "V = {}")
case True
@@ -1059,7 +1059,7 @@
qed

proposition extend_to_affine_basis:
-  fixes S V :: "'n::euclidean_space set"
+  fixes S V :: "'n::real_vector set"
assumes "\<not> affine_dependent S" "S \<subseteq> V"
obtains T where "\<not> affine_dependent T" "S \<subseteq> T" "T \<subseteq> V" "affine hull T = affine hull V"
proof (cases "S = {}")
@@ -1073,13 +1073,13 @@

subsection \<open>Affine Dimension of a Set\<close>

-definition\<^marker>\<open>tag important\<close> aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
+definition\<^marker>\<open>tag important\<close> aff_dim :: "('a::real_vector) set \<Rightarrow> int"
where "aff_dim V =
(SOME d :: int.
\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"

lemma aff_dim_basis_exists:
-  fixes V :: "('n::euclidean_space) set"
+  fixes V :: "('n::real_vector) set"
shows "\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1"
proof -
obtain B where "\<not> affine_dependent B \<and> affine hull B = affine hull V"

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.