Nuprl Definition : class-le-before

class-le-before(X;es;e) == ∪e'∈≤loc(e).X es e'

Definitions occuring in Statement : es-le-before: ≤loc(e), apply: f a, bag-combine: ∪x∈bs.f[x]
FDL editor aliases : class-le-before
class-le-before(X;es;e) == \mcup{}e'\mmember{}\mleq{}loc(e).X es e' Date html generated: 2015_07_17-PM-00_14_33 Last ObjectModification: 2012_02_25-PM-01_11_58 Home Index