Nuprl Lemma : member-eclass-eclass3

[Info,B,C:Type]. ∀[X:EClass(B ─→ C)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(↑e ∈b eclass3(X;Y);(↑e ∈b X) ∧ (↑e ∈b Y))


Proof




Definitions occuring in Statement :  eclass3: eclass3(X;Y) member-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E assert: b uiff: uiff(P;Q) uall: [x:A]. B[x] and: P ∧ Q function: x:A ─→ B[x] universe: Type
Lemmas :  assert-member-eclass eclass3-classrel classrel_wf assert_witness member-eclass_wf assert_wf eclass3_wf exists_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf

Latex:
\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  C)].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    uiff(\muparrow{}e  \mmember{}\msubb{}  eclass3(X;Y);(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\muparrow{}e  \mmember{}\msubb{}  Y))



Date html generated: 2015_07_23-AM-11_28_22
Last ObjectModification: 2015_01_28-PM-11_13_06

Home Index