Nuprl Definition : tfunequiv

tfunequiv(X;Y) ==
  <λa,x. let _,_,refl,_,_ = Y in refl (a x)
  , λa,b,%,x. let _,_,_,sym,_ = Y in sym (a x) (b x) (% x)
  , λa,b,c,%,%2,x. let _,_,_,_,trans = Y in trans (a x) (b x) (c x) (% x) (%2 x)>

Definitions occuring in Statement : spreadn: let a,b,c,d,e = u in v[a; b; c; d; e], apply: f a, lambda: λx.A[x], pair: <a, b>
Definitions occuring in definition : apply: f a, spreadn: let a,b,c,d,e = u in v[a; b; c; d; e], lambda: λx.A[x], pair: <a, b>
FDL editor aliases : tfunequiv

Latex:
tfunequiv(X;Y) == <\mlambda{}a,x. let $_{}$,$_{}$,refl,$_{}$,\mbackslash{}ff2\000C4_{}$ = Y in refl (a x) , \mlambda{}a,b,\%,x. let $_{}$,$_{}$,$_{}$,sym,\000C$_{}$ = Y in sym (a x) (b x) (\% x) , \mlambda{}a,b,c,\%,\%2,x. let $_{}$,$_{}$,$_{}$\000C,$_{}$,trans = Y in trans (a x) (b x) (c x) (\% x) (\%2 x)> Date html generated: 2018_07_29-AM-09_48_34 Last ObjectModification: 2018_06_21-AM-10_35_25 Theory : inner!product!spaces Home Index