Nuprl Definition : refl_cl
Eo == λx,y. ((x = y ∈ T) ∨ (E x y))
Definitions occuring in Statement :
or: P ∨ Q,
apply: f a,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
or: P ∨ Q,
equal: s = t ∈ T,
apply: f a
Latex:
E\msupzero{} == \mlambda{}x,y. ((x = y) \mvee{} (E x y))
Date html generated:
2016_05_15-PM-00_01_27
Last ObjectModification:
2015_09_23-AM-06_23_43
Theory : gen_algebra_1
Home
Index