Nuprl Definition : sqntype
sqntype(n;T) == ∀x,y:Base. ((x = y ∈ T) ⇒ (x ~n y))
Definitions occuring in Statement :
all: ∀x:A. B[x],
implies: P ⇒ Q,
base: Base,
sqequal_n: s ~n t,
equal: s = t ∈ T
Definitions occuring in definition :
sqntype: Error :sqntype def,
all: ∀x:A. B[x],
base: Base,
implies: P ⇒ Q,
equal: s = t ∈ T,
sqequal_n: s ~n t
FDL editor aliases :
sqntype
sqntype
Latex:
sqntype(n;T) == \mforall{}x,y:Base. ((x = y) {}\mRightarrow{} (x \msim{}n y))
Date html generated:
2019_06_20-AM-11_33_54
Last ObjectModification:
2018_08_17-PM-03_27_33
Theory : int_1
Home
Index