Nuprl Definition : princ_ideal
(a)r == λc.∃b:|r|. (c = (a * b) ∈ |r|)
Definitions occuring in Statement :
rng_times: *,
rng_car: |r|,
infix_ap: x f y,
exists: ∃x:A. B[x],
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
exists: ∃x:A. B[x],
equal: s = t ∈ T,
rng_car: |r|,
infix_ap: x f y,
rng_times: *
Latex:
(a)r == \mlambda{}c.\mexists{}b:|r|. (c = (a * b))
Date html generated:
2016_05_15-PM-00_23_07
Last ObjectModification:
2015_09_23-AM-06_25_52
Theory : rings_1
Home
Index