Nuprl Lemma : alle-le_wf

[es:EO]. ∀[e':E]. ∀[P:{e:E| loc(e) loc(e') ∈ Id}  ─→ ℙ].  (∀e≤e'.P[e] ∈ ℙ)


Proof




Definitions occuring in Statement :  alle-le: e≤e'.P[e] es-loc: loc(e) es-E: E event_ordering: EO Id: Id uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T set: {x:A| B[x]}  function: x:A ─→ B[x] equal: t ∈ T
Lemmas :  all_wf es-E_wf es-le_wf es-le-loc Id_wf es-loc_wf
\mforall{}[es:EO].  \mforall{}[e':E].  \mforall{}[P:\{e:E|  loc(e)  =  loc(e')\}    {}\mrightarrow{}  \mBbbP{}].    (\mforall{}e\mleq{}e'.P[e]  \mmember{}  \mBbbP{})



Date html generated: 2015_07_17-AM-08_46_39
Last ObjectModification: 2015_01_27-PM-02_26_20

Home Index