Nuprl - Proof: iter perm cycles uniform

(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some positive iteration of any finite permutation is the identity function.

At: iter perm cycles uniform

, f:(

k inj

k).

k. f{

i}(u) = u

By:	SimilarTo Thm* k:, f:(k inj k), u:k. i:. f{i}(u) = u ...w

Generated subgoal:

1 1. k :
2. f : k inj k
3. u:k. i:. f{i}(u) = u
i:. u:k. f{i}(u) = u
13 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc