Nuprl Lemma : poss-le_wf
∀[poss:EO ─→ ℙ']. ∀[e1,e2:PossibleEvent(poss)]. (e1 ≤ e2 ∈ ℙ')
Proof
Definitions occuring in Statement :
poss-le: e1 ≤ e2,
possible-event: PossibleEvent(poss),
event_ordering: EO,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
function: x:A ─→ B[x]
Lemmas :
event_ordering_wf,
es-le_wf,
subtype_rel-equal,
es-E_wf,
squash_wf,
true_wf,
iff_weakening_equal
\mforall{}[poss:EO {}\mrightarrow{} \mBbbP{}']. \mforall{}[e1,e2:PossibleEvent(poss)]. (e1 \mleq{} e2 \mmember{} \mBbbP{}')
Date html generated:
2015_07_17-AM-08_52_24
Last ObjectModification:
2015_02_04-PM-05_55_38
Home
Index