Re: [mizar] properties

[Josef Urban <josef.urban@gmail.com>]

identity?

Aren't these all keywords obsolete now that there is "identify" in Mizar?

Best,
Josef

On Wed, Aug 10, 2011 at 3:12 PM, Artur Kornilowicz
<arturk@math.uwb.edu.pl> wrote:
> 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?
>
> Best regards
> Artur
>