Nuprl Definition : permutation
permutation(T;L1;L2) ==  ∃f:ℕ||L1|| ⟶ ℕ||L1||. (Inj(ℕ||L1||;ℕ||L1||;f) ∧ (L2 = (L1 o f) ∈ (T List)))
Definitions occuring in Statement : 
permute_list: (L o f)
, 
length: ||as||
, 
list: T List
, 
inject: Inj(A;B;f)
, 
int_seg: {i..j-}
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
, 
function: x:A ⟶ B[x]
, 
natural_number: $n
, 
equal: s = t ∈ T
Definitions occuring in definition : 
exists: ∃x:A. B[x]
, 
function: x:A ⟶ B[x]
, 
and: P ∧ Q
, 
inject: Inj(A;B;f)
, 
int_seg: {i..j-}
, 
natural_number: $n
, 
length: ||as||
, 
equal: s = t ∈ T
, 
list: T List
, 
permute_list: (L o f)
FDL editor aliases : 
permutation
Latex:
permutation(T;L1;L2)  ==    \mexists{}f:\mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L1||.  (Inj(\mBbbN{}||L1||;\mBbbN{}||L1||;f)  \mwedge{}  (L2  =  (L1  o  f)))
Date html generated:
2016_05_14-PM-02_17_40
Last ObjectModification:
2016_01_05-PM-00_20_22
Theory : list_1
Home
Index