Nuprl Lemma : Q-R-glued-first

`∀[Info:Type]`
`  ∀es:EO+(Info)`
`    ∀[Q,R:E ─→ E ─→ ℙ]. ∀[A,B:Type].`
`      ∀Ias:EClass(A) List. ∀Ibs:EClass(B) List. ∀f:E(first-class(Ias)) ─→ B.`
`        ((∀i:ℕ||Ias||. Ias[i]:Q →─f─→  Ibs[i]:R)`
`           `` first-class(Ias):Q →─f─→  first-class(Ibs):R `
`              supposing (∀Ia1,Ia2∈Ias.  ∀e,e':E.`
`                                          ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))) supposi\000Cng `
`           ((||Ias|| = ||Ibs|| ∈ ℤ) and `
`           (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0) and `
`           (∀Ia1,Ia2∈Ias.  Ia1 ∩ Ia2 = 0))`

Proof

Definitions occuring in Statement :  Q-R-glued: `Ia:Qa →─f─→  Ib:Rb` es-interface-disjoint: `X ∩ Y = 0` es-E-interface: `E(X)` first-class: `first-class(L)` in-eclass: `e ∈b X` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-E: `E` pairwise: `(∀x,y∈L.  P[x; y])` select: `L[n]` length: `||as||` list: `T List` int_seg: `{i..j-}` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ─→ B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Lemmas :  list_induction eclass_wf all_wf list_wf es-E_wf event-ordering+_subtype es-E-interface_wf first-class_wf top_wf subtype_rel_list es-interface-subtype_rel2 isect_wf pairwise_wf es-interface-disjoint_wf length_wf int_seg_wf Q-R-glued_wf select_wf sq_stable__le less_than_transitivity1 le_weakening subtype_rel_dep_function es-E-interface-first-class assert_wf in-eclass_wf not_wf event-ordering+_wf length_of_nil_lemma stuck-spread base_wf list-cases less_than_irreflexivity equal-wf-base product_subtype_list length_of_cons_lemma cons_wf length_cons non_neg_length length_wf_nat equal-wf-base-T nil_wf Q-R-glued-empty reduce_nil_lemma equal_wf le_weakening2 less_than_transitivity2 reduce_cons_lemma es-E-interface-conditional-subtype2 cond-class_wf pairwise-cons lelt_wf select_cons_tl_sq Q-R-glued-conditional subtype_rel_self l_all_iff l_member_wf l_exists_iff is-first-class or_wf es-interface-conditional-domain-iff decidable__assert Q-R-glues_functionality Q-R-glues_wf es-interface-predicate_wf rel-restriction_wf rel_or_wf

Latex:
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[Q,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A,B:Type].
\mforall{}Ias:EClass(A)  List.  \mforall{}Ibs:EClass(B)  List.  \mforall{}f:E(first-class(Ias))  {}\mrightarrow{}  B.
((\mforall{}i:\mBbbN{}||Ias||.  Ias[i]:Q  \mrightarrow{}{}f{}\mrightarrow{}    Ibs[i]:R)
{}\mRightarrow{}  first-class(Ias):Q  \mrightarrow{}{}f{}\mrightarrow{}    first-class(Ibs):R
supposing  (\mforall{}Ia1,Ia2\mmember{}Ias.    \mforall{}e,e':E.
((\mneg{}(Q  e  e'))  \mwedge{}  (\mneg{}(Q  e'  e)))  supposing
((\muparrow{}e'  \mmember{}\msubb{}  Ia2)  and
(\muparrow{}e  \mmember{}\msubb{}  Ia1))))  supposing
((||Ias||  =  ||Ibs||)  and
(\mforall{}Ib1,Ib2\mmember{}Ibs.    Ib1  \mcap{}  Ib2  =  0)  and
(\mforall{}Ia1,Ia2\mmember{}Ias.    Ia1  \mcap{}  Ia2  =  0))

Date html generated: 2015_07_21-PM-04_13_22
Last ObjectModification: 2015_02_02-PM-06_44_51

Home Index