Nuprl Definition : function-eq
function-eq(A;a.B[a];f;g) == ∀[a,b:Base]. (f a) = (g b) ∈ B[a] supposing a = b ∈ A
Definitions occuring in Statement :
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
apply: f a,
base: Base,
equal: s = t ∈ T
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
base: Base,
uimplies: b supposing a,
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
function-eq
Latex:
function-eq(A;a.B[a];f;g) == \mforall{}[a,b:Base]. (f a) = (g b) supposing a = b
Date html generated:
2016_05_13-PM-03_53_28
Last ObjectModification:
2015_09_22-PM-05_45_30
Theory : per!type
Home
Index