Nuprl Rule : independent_pairFormation

H  ⊢ A × ext <a, b>

  BY independent_pairFormation ()
  
  H  ⊢ ext a
  H  ⊢ ext b



Definitions occuring in rule :  product: x:A × B[x] pair: <a, b>

Latex:
H    \mvdash{}  A  \mtimes{}  B  ext  <a,  b>

    BY  independent\_pairFormation  ()
   
    H    \mvdash{}  A  ext  a
    H    \mvdash{}  B  ext  b



Date html generated: 2016_12_14-AM-08_53_26
Last ObjectModification: 2015_11_25-PM-03_37_45

Theory : rules


Home Index