---

Step * of Lemma brouwer_prin_fun_imp_num

brouwer_prin_for_fun_27_1ax{i:l}()  brouwer_prin_for_num_27_2{i:l}()
BY
{ (Unfold `brouwer_prin_for_num_27_2` 0 THEN Auto) }

1
1. brouwer_prin_for_fun_27_1ax{i:l}()@i'
2. A :       @i'
3. f:  . b:. (A f b)@i
 T: List  . f:  . !y:. ((T mklist(y;f)) > 0)  (A f (T mklist(y;f)--1))


brouwer\_prin\_for\_fun\_27\_1ax\{i:l\}()  {}\mRightarrow{}  brouwer\_prin\_for\_num\_27\_2\{i:l\}()


By

(Unfold  `brouwer\_prin\_for\_num\_27\_2`  0  THEN  Auto)



Home Index