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