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



On Sat Oct 17, 2020 at 2:59 PM CEST, Lawrence Paulson wrote:
> Can you find any other theorems based on this definition that can
> similarly be generalised? It seems odd if that is the only one.

There seems to be a significant fraction that uses the euclidean_space
constraint to deduce that a basis is finite, which is not true in an
infinite-dimensional vector space. This raises a question of what the
value of aff_dim should be in an infinite dimension, if any - currently
card returns 0 in this case, with excruciating results.

Adding a `finite B` condition to aff_dim wouldn't really work, as the
unspecified value this would result in wouldn't allow you to infer
'aff_dim S = -1 --> finite B'.

Maybe it would make sense to define a typeclass for finite-dimensional
real vector spaces, as an analogue of the
finite_dimensional_vector_space locale?

Regards,
Jakub Kądziołka




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