Nuprl Rule : independent_pairFormation
H ⊢ A × B ext <a, b>
BY independent_pairFormation ()
H ⊢ A ext a
H ⊢ B 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:
2019_06_20-PM-04_11_43
Last ObjectModification:
2015_11_25-PM-03_37_45
Theory : rules
Home
Index