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