[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] 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/