*To*: Jakub Kądziołka <kuba at kadziolka.net>*Subject*: Re: [isabelle] Weak lemmas in HOL-Analysis.Affine*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sat, 17 Oct 2020 13:59:29 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <C6F64IXDB3SH.3BJPKLWWVZ9AQ@gravity>*References*: <C6F64IXDB3SH.3BJPKLWWVZ9AQ@gravity>

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

**Follow-Ups**:**Re: [isabelle] Weak lemmas in HOL-Analysis.Affine***From:*Jakub Kądziołka

**References**:**Re: [isabelle] Weak lemmas in HOL-Analysis.Affine***From:*Jakub Kądziołka

- Previous by Date: Re: [isabelle] Weak lemmas in HOL-Analysis.Affine
- Next by Date: Re: [isabelle] Weak lemmas in HOL-Analysis.Affine
- Previous by Thread: Re: [isabelle] Weak lemmas in HOL-Analysis.Affine
- Next by Thread: Re: [isabelle] Weak lemmas in HOL-Analysis.Affine
- Cl-isabelle-users October 2020 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list