Nuprl Lemma : Q-R-glued-conditional

    ∀[Q1,Q2,R:E ─→ E ─→ ℙ]. ∀[A,B:Type].
      ∀Ia1,Ia2:EClass(A). ∀Ib1,Ib2:EClass(B). ∀f:E([Ia1?Ia2]) ─→ B.
        (Ia1:Q1 →─f─→  Ib1:R  Ia2:Q2 →─f─→  Ib2:R  [Ia1?Ia2]:Q1|{Ia1} ∨ Q2|{Ia2} →─f─→  [Ib1?Ib2]:R) supposing 
           (Ib1 ∩ Ib2 and 
           Ia1 ∩ Ia2 0)


Definitions occuring in Statement :  Q-R-glued: Ia:Qa →─f─→  Ib:Rb es-interface-disjoint: X ∩ 0 es-E-interface: E(X) es-interface-predicate: {I} cond-class: [X?Y] eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E rel-restriction: R|P rel_or: R1 ∨ R2 uimplies: supposing a uall: [x:A]. B[x] prop: all: x:A. B[x] implies:  Q function: x:A ─→ B[x] universe: Type
Lemmas :  assert_wf in-eclass_wf es-E_wf event-ordering+_subtype es-interface-subtype_rel2 cond-class_wf es-E-interface-conditional-subtype1 es-E-interface_wf Q-R-glues-property subtype_rel_dep_function es-E-interface-conditional-subtype2 Q-R-glued_wf es-interface-disjoint_wf top_wf eclass_wf event-ordering+_wf conditional_wf-interface2 Q-R-glues_wf rel_or_wf rel-restriction_wf es-interface-predicate_wf Q-R-glues-conditional

        \mforall{}[Q1,Q2,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A,B:Type].
            \mforall{}Ia1,Ia2:EClass(A).  \mforall{}Ib1,Ib2:EClass(B).  \mforall{}f:E([Ia1?Ia2])  {}\mrightarrow{}  B.
                (Ia1:Q1  \mrightarrow{}{}f{}\mrightarrow{}    Ib1:R
                      {}\mRightarrow{}  Ia2:Q2  \mrightarrow{}{}f{}\mrightarrow{}    Ib2:R
                      {}\mRightarrow{}  [Ia1?Ia2]:Q1|\{Ia1\}  \mvee{}  Q2|\{Ia2\}  \mrightarrow{}{}f{}\mrightarrow{}    [Ib1?Ib2]:R)  supposing 
                      (Ib1  \mcap{}  Ib2  =  0  and 
                      Ia1  \mcap{}  Ia2  =  0)

Date html generated: 2015_07_21-PM-04_13_00
Last ObjectModification: 2015_01_27-PM-05_41_10

Home Index