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

Can you find any other theorems based on this definition that can similarly be generalised? It seems odd if that is the only one. And it would be nice to have some compensation for the effort that will be needed to add type class constraints for quite a few other theorems.


> On 17 Oct 2020, at 13:34, Jakub Kądziołka <kuba at> wrote:
> 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.

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