Nuprl Definition : sq_type
SQType(T) == ∀x,y:T. ((x = y ∈ T) ⇒ {x ~ y})
Definitions occuring in Statement :
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
sqequal: s ~ t,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T,
guard: {T},
sqequal: s ~ t
FDL editor aliases :
sq_type
Latex:
SQType(T) == \mforall{}x,y:T. ((x = y) {}\mRightarrow{} \{x \msim{} y\})
Date html generated:
2016_05_13-PM-03_19_49
Last ObjectModification:
2016_01_04-AM-10_24_57
Theory : sqequal_1
Home
Index