Nuprl Definition : image-per
image-per(A;f) == λx,y. usquash(TC(λx,y. ∃a,b:Base. ((a = b ∈ A) ∧ (x ~ f a) ∧ (y ~ f b))) x y)
Definitions occuring in Statement :
transitive-closure: TC(R),
usquash: usquash(T),
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
base: Base,
sqequal: s ~ t,
equal: s = t ∈ T
Definitions occuring in definition :
usquash: usquash(T),
transitive-closure: TC(R),
lambda: λx.A[x],
exists: ∃x:A. B[x],
base: Base,
equal: s = t ∈ T,
and: P ∧ Q,
sqequal: s ~ t,
apply: f a
FDL editor aliases :
image-per
Latex:
image-per(A;f) == \mlambda{}x,y. usquash(TC(\mlambda{}x,y. \mexists{}a,b:Base. ((a = b) \mwedge{} (x \msim{} f a) \mwedge{} (y \msim{} f b))) x y)
Date html generated:
2019_06_20-PM-02_02_30
Last ObjectModification:
2018_09_05-PM-08_26_26
Theory : relations2
Home
Index