Nuprl Definition : rv-le
X ≤ Y == ∀s:ℕn ─→ Outcome. ((X s) ≤ (Y s))
Definitions occuring in Statement :
p-outcome: Outcome,
int_seg: {i..j-},
all: ∀x:A. B[x],
apply: f a,
function: x:A ─→ B[x],
natural_number: $n
Definitions :
all: ∀x:A. B[x],
function: x:A ─→ B[x],
int_seg: {i..j-},
natural_number: $n,
p-outcome: Outcome,
qle: Error :qle,
apply: f a
FDL editor aliases :
rv-le
X \mleq{} Y == \mforall{}s:\mBbbN{}n {}\mrightarrow{} Outcome. ((X s) \mleq{} (Y s))
Date html generated:
2015_07_17-AM-07_59_42
Last ObjectModification:
2008_02_27-PM-05_49_13
Home
Index