Nuprl Definition : dep-fun-equiv

dep-fun-equiv(X;x,a,b.E[x; a; b];f;g) == ∀x:X. E[x; f x; g x]

Definitions occuring in Statement : all: ∀x:A. B[x], apply: f a
Definitions occuring in definition : apply: f a, all: ∀x:A. B[x]
FDL editor aliases : dep-fun-equiv

Latex:
dep-fun-equiv(X;x,a,b.E[x; a; b];f;g) == \mforall{}x:X. E[x; f x; g x] Date html generated: 2017_09_29-PM-05_48_14 Last ObjectModification: 2017_09_07-PM-03_19_26 Theory : quot_1 Home Index