Nuprl Definition : double-negation-shift
DNSi.A[i] == (∀i:ℕ. (¬¬A[i])) ⇒ (¬¬(∀i:ℕ. A[i]))
Definitions occuring in Statement :
nat: ℕ,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q
Definitions occuring in definition :
implies: P ⇒ Q,
not: ¬A,
all: ∀x:A. B[x],
nat: ℕ
FDL editor aliases :
double-negation-shift
Latex:
DNSi.A[i] == (\mforall{}i:\mBbbN{}. (\mneg{}\mneg{}A[i])) {}\mRightarrow{} (\mneg{}\mneg{}(\mforall{}i:\mBbbN{}. A[i]))
Date html generated:
2016_05_15-PM-03_20_42
Last ObjectModification:
2015_09_23-AM-07_42_52
Theory : general
Home
Index