Step
*
of Lemma
permutation-map
∀[A:Type]. ∀L1,L2:A List. (permutation(A;L1;L2)
⇒ (∀[B:Type]. ∀f:A ⟶ B. permutation(B;map(f;L1);map(f;L2))))
BY
{ (Auto
THEN RepeatFor 3 (ParallelOp -3)
THEN Try (((HypSubst (-3) 0 THENM BLemma `list_extensionality`) THEN Auto))
THEN RWW "length-map permute_list_length map_select permute_list_select" 0
THEN Auto
THEN (All (RWW "length-map permute_list_length") THEN Auto THEN Auto')⋅) }
Latex:
Latex:
\mforall{}[A:Type]
\mforall{}L1,L2:A List.
(permutation(A;L1;L2) {}\mRightarrow{} (\mforall{}[B:Type]. \mforall{}f:A {}\mrightarrow{} B. permutation(B;map(f;L1);map(f;L2))))
By
Latex:
(Auto
THEN RepeatFor 3 (ParallelOp -3)
THEN Try (((HypSubst (-3) 0 THENM BLemma `list\_extensionality`) THEN Auto))
THEN RWW "length-map permute\_list\_length map\_select permute\_list\_select" 0
THEN Auto
THEN (All (RWW "length-map permute\_list\_length") THEN Auto THEN Auto')\mcdot{})
Home
Index