Re: [isabelle] Weak lemmas in HOL-Analysis.Affine



On Sat Oct 17, 2020 at 12:22 PM CEST, Lawrence Paulson wrote:
> 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

aff_dim_basis_exists doesn't require euclidean_space. In fact, this
restriction on the definition is what motivated my investigation in the
first place, as I want to speak of an affine dimension in an arbitrary
real vector space in my formalization, and extracting a basis is what
I'm using the assumption for.

Regards,
Jakub Kądziołka




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