Nuprl Rule : perfunctionExtensionality

H  ⊢ f = g ∈ per-function(A;x.B)

  BY perfunctionExtensionality !parameter{i:l} u ()
  
  H u:A ⊢ (f u) = (g u) ∈ B[u/x]
  H  ⊢ A = A ∈ Type


Definitions occuring in rule :  per-function: per-function(A;a.B[a]),  apply: f a,  equal: s = t ∈ T,  universe: Type,  axiom: Ax
Latex:
H    \mvdash{}  f  =  g

    BY  perfunctionExtensionality  !parameter\{i:l\}  u  ()
   
    H  u:A  \mvdash{}  (f  u)  =  (g  u)
    H    \mvdash{}  A  =  A


Date html generated: 2017_09_29-PM-05_45_07
Last ObjectModification: 2015_11_25-PM-03_51_08

Theory : rules


Home Index