Re: properties

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

-- 
Jesse Alama
http://centria.di.fct.unl.pt/~alama/