Nuprl Lemma : ranked-eo-causl
∀[L,rk,a,b:Top]. ((a < b) ~ ↓rk a < rk b)
Proof
Definitions occuring in Statement :
ranked-eo: ranked-eo(L;rk)
,
es-causl: (e < e')
,
less_than: a < b
,
uall: ∀[x:A]. B[x]
,
top: Top
,
squash: ↓T
,
apply: f a
,
sqequal: s ~ t
Lemmas :
rec_select_update_lemma,
top_wf
Latex:
\mforall{}[L,rk,a,b:Top]. ((a < b) \msim{} \mdownarrow{}rk a < rk b)
Date html generated:
2015_07_21-PM-04_43_41
Last ObjectModification:
2015_01_27-PM-04_57_08
Home
Index