Re: Re: properties

On Wed, 10 Aug 2011, Jesse Alama wrote:

> On 2011-08-10 13:12:32 +0000, Artur Kornilowicz said:
>
>> In mathematics there are unary operations (let say f) satisfying property
>> 
>> f^m(x) = f^n(x).
>> 
>> Some of them have commonly used names, like
>> 
>> for m = 2, n = 1, that is f(f(x)) = f(x) - projectivity
>> 
>> for m = 2, n = 0, that is f(f(x)) = x - involutiveness
>> 
>> 
>> 
>> In the MML there are theorems about operations satisfying the property
>> for m = 1 and n = 0, for example:
>> 
>> theorem
>>    for m being Nat holds m = abs m
>> 
>> theorem
>>   for T being non empty TopSpace, a being Point of T,
>>       P being constant Path of a,a
>>   holds - P = P
>> 
>> We are thinking about implementation of the property (m=1,n=0) in
>> Mizar, and we are looking for an appropriate name for it.
>> 
>> Any suggestions?
>
> Josef's suggestion of "identity" works.  Here's one way to write those
> two examples, in some freewheeling notation:
>
> registration
>  abs[Integer] is identity across Nat;
> end;
>
> registration
>  let T be non empty TopSpace,
>      a be Point of T;
>  -[constant Path of a,a] is identity across Path of a,a;
> end;
>
> Jesse


I think we should rather use

registration
  let n be Nat;
  identity of -n;
end;

what is similar to 'sethood of'.

Artur