Step * 1 of Lemma mon_for_functionality_wrt_permr


1. IAbMonoid
2. Type
3. as List
4. as' List
5. A ⟶ |g|
6. f' A ⟶ |g|
7. as ≡(A) as'
8. ∀x:A. (mem_f(A;x;as)  (f[x] f'[x] ∈ |g|))
⊢ (Π map(λx:A. f[x];as)) (Π map(λx:A. f'[x];as')) ∈ |g|
BY
(% Important for later that we use RevHypC rather than HypC %  Unfold `tlambda` THEN RWH (RevHypC 7) THEN Auto) }

1
1. IAbMonoid
2. Type
3. as List
4. as' List
5. A ⟶ |g|
6. f' A ⟶ |g|
7. as ≡(A) as'
8. ∀x:A. (mem_f(A;x;as)  (f[x] f'[x] ∈ |g|))
⊢ (Π map(λx.f[x];as)) (Π map(λx.f'[x];as)) ∈ |g|


Latex:


Latex:

1.  g  :  IAbMonoid
2.  A  :  Type
3.  as  :  A  List
4.  as'  :  A  List
5.  f  :  A  {}\mrightarrow{}  |g|
6.  f'  :  A  {}\mrightarrow{}  |g|
7.  as  \mequiv{}(A)  as'
8.  \mforall{}x:A.  (mem\_f(A;x;as)  {}\mRightarrow{}  (f[x]  =  f'[x]))
\mvdash{}  (\mPi{}  map(\mlambda{}x:A.  f[x];as))  =  (\mPi{}  map(\mlambda{}x:A.  f'[x];as'))


By


Latex:
(\%  Important  for  later  that  we  use  RevHypC  rather  than  HypC  \% 
  Unfold  `tlambda`  0
  THEN  RWH  (RevHypC  7)  0
  THEN  Auto)




Home Index