Nuprl Definition : topfuneq
topfuneq(X;Y;f;g) == ∀x:|X|. topeq(Y;f x;g x)
Definitions occuring in Statement :
topeq: topeq(X;a;b),
toptype: |X|,
all: ∀x:A. B[x],
apply: f a
Definitions occuring in definition :
apply: f a,
topeq: topeq(X;a;b),
toptype: |X|,
all: ∀x:A. B[x]
FDL editor aliases :
topfuneq
Latex:
topfuneq(X;Y;f;g) == \mforall{}x:|X|. topeq(Y;f x;g x)
Date html generated:
2018_07_29-AM-09_48_19
Last ObjectModification:
2018_06_21-AM-10_11_30
Theory : inner!product!spaces
Home
Index