Nuprl Definition : frs-refines
frs-refines(p;q) == (∀x∈q.(∃y∈p. x = y))
Definitions occuring in Statement :
req: x = y,
l_exists: (∃x∈L. P[x]),
l_all: (∀x∈L.P[x])
Definitions occuring in definition :
l_all: (∀x∈L.P[x]),
l_exists: (∃x∈L. P[x]),
req: x = y
FDL editor aliases :
frs-refines
frs-refines
Latex:
frs-refines(p;q) == (\mforall{}x\mmember{}q.(\mexists{}y\mmember{}p. x = y))
Date html generated:
2016_05_18-AM-08_52_08
Last ObjectModification:
2015_09_23-AM-09_08_24
Theory : reals
Home
Index