Nuprl Definition : image-type

Nuprl Definition : image-type_def

There are four rules about this primitive type.
imageEquality
    which implies that Image(A,f) is a type if A ∈ Type and f ∈ Base;
imageMemberEquality
    which implies that the terms ⌜f a⌝, a ∈ A are members of Image(A,f);
imageElimination  says that these are the only members of Image(A,f)
    so ⌜x ∈ Image(A,f)⌝ can be replaced by ⌜f a⌝ for a "hiddden" a ∈ A;
imageEqInduction
   If forall a,b ∈ Base. (f a ∈ T  and a=b ∈ A  implies f(a)=f(b) ∈ T) then
   the equivalence class of f t1 in Image(A,f) contains
   the equivalence class of f t1 in T⋅

Image(T,f) == PRIMITIVE

Rules referencing : imageEquality, imageMemberEquality, imageElimination, imageEqInduction, equalityEqualityBase
FDL editor aliases : image

Latex:
Image(T,f) == PRIMITIVE Date html generated: 2016_07_08-PM-04_46_27 Last ObjectModification: 2015_06_28-PM-00_06_44 Theory : core_1 Home Index