Re: [isabelle] Degree of an almost everywhere constant function



The only thing I am aware of is HOL-Library.Poly_Mapping, which you are
probably aware of, seeing as it has your name at the top.

Manuel


On 15/10/2020 16:41, Florian Haftmann wrote:
> Hi all,
> 
> in certain applications (most prominently polynomials) almost everywhere
> constant functions nat => 'a play a critical role, and any almost
> everywhere constant function can be assigned a degree, i. e. the highest
> n such that for any higher n the function is constant.
> 
> Is there any stand-alone formalizsation of this concept?
> 
> Cheers,
> 	Florian
> 

Attachment: signature.asc
Description: OpenPGP digital signature



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