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