Nuprl Definition : meqfun
meqfun(d;A;f;g) ==  ∀a:A. f a ≡ g a
Definitions occuring in Statement : 
meq: x ≡ y
, 
all: ∀x:A. B[x]
, 
apply: f a
Definitions occuring in definition : 
all: ∀x:A. B[x]
, 
meq: x ≡ y
, 
apply: f a
FDL editor aliases : 
meqfun
Latex:
meqfun(d;A;f;g)  ==    \mforall{}a:A.  f  a  \mequiv{}  g  a
Date html generated:
2019_10_30-AM-06_28_47
Last ObjectModification:
2019_10_02-AM-10_03_55
Theory : reals
Home
Index