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.

Larry

> 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 MHonArc.