DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  Replace value k by f(m) in f == Replace values x s.t. x=k by f(m) in f

is mentioned by

Thm*  Bij((m+1); (k+1); f)  Bij(m; k; Replace value k by f(m) in f)[delete_fenum_value_is_fenum]
Thm*  Inj((m+1); (k+1); f)  Inj(m; k; Replace value k by f(m) in f)[delete_fenum_value_is_inj]
Thm*  Inj((m+1); (k+1); f)
Thm*  
Thm*  (i:m. f(i) = k  (Replace value k by f(m) in f)(i) = f(i) k)		[delete_fenum_value_comp2]
Thm*  Inj((m+1); (k+1); f)
Thm*  
Thm*  (i:m. f(i) = k  (Replace value k by f(m) in f)(i) = f(m) k)		[delete_fenum_value_comp1]
Thm*  Bij({u:| P(u) }; {v:| Q(v) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  (Bij({u:| P(u) & u = m }; {v:| Q(v) & v = k };
Thm*  (Bij(Replace value k by f(m) in f))		[delete_fenum_value_is_fenum_gen]
Thm*  Inj({u:| P(u) }; {v:| Q(v) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  (Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
Thm*  (Inj(Replace value k by f(m) in f))		[delete_fenum_value_is_inj_gen]
Thm*  Inj({u:| P(u) }; {v:| Q(v) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  ((Replace value k by f(m) in f)
Thm*  ( {u:| P(u) & u = m }{v:| Q(v) & v = k }
Thm*  (& Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
Thm*  (& Inj(Replace value k by f(m) in f))		[delete_fenum_value_is_inj_genW]
Thm*  Inj({u:| P(u) }; {u:| Q(u) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }.
Thm*  (f(i) = k
Thm*  (
Thm*  ((Replace value k by f(m) in f)(i) = f(i)  {v:| Q(v) & v = k })		[delete_fenum_value_comp2_gen]
Thm*  Inj({u:| P(u) }; {u:| Q(u) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }.
Thm*  (f(i) = k
Thm*  (
Thm*  ((Replace value k by f(m) in f)(i) = f(m)  {v:| Q(v) & v = k })		[delete_fenum_value_comp1_gen]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

DiscreteMath Sections DiscrMathExt Doc