Nuprl Rule : functionExtensionality
H ⊢ f = g ∈ (x:A ⟶ B)
BY functionExtensionality !parameter{i:l} u ()
H u:A ⊢ (f u) = (g u) ∈ B[u/x]
H ⊢ A = A ∈ Type
Definitions occuring in rule :
function: x:A ⟶ B[x],
apply: f a,
equal: s = t ∈ T,
universe: Type,
axiom: Ax
Latex:
H \mvdash{} f = g
BY functionExtensionality !parameter\{i:l\} u ()
H u:A \mvdash{} (f u) = (g u)
H \mvdash{} A = A
Date html generated:
2019_06_20-PM-04_11_45
Last ObjectModification:
2018_09_17-PM-02_20_36
Theory : rules
Home
Index