Re: [isabelle] Weak lemmas in HOL-Analysis.Affine
I’m happy with your suggestion in theorems, but does it make sense in this definition? Practically all of the theorems still require euclidean_space, so changing the definition as you suggest will merely force people to write more explicit type class constraints.
> On 16 Oct 2020, at 15:07, Jakub Kądziołka <kuba at kadziolka.net> wrote:
> 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)"
This archive was generated by a fusion of
Pipermail (Mailman edition) and