Nuprl Definition : l_all_since
(∀x≥a∈L.P[x]) == P[a] ∧ (∀b:T. (a before b ∈ L ⇒ P[b]))
Definitions occuring in Statement :
l_before: x before y ∈ l,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
l_before: x before y ∈ l
FDL editor aliases :
l_all_since
Latex:
(\mforall{}x\mgeq{}a\mmember{}L.P[x]) == P[a] \mwedge{} (\mforall{}b:T. (a before b \mmember{} L {}\mRightarrow{} P[b]))
Date html generated:
2016_05_15-PM-01_55_57
Last ObjectModification:
2015_09_23-AM-07_37_29
Theory : list!
Home
Index