Nuprl Definition : DCC
DCC (descending chain condition) says that there is no infinte
descending chain for the given relation.⋅
DCC(T;<) == ∀f:ℕ ⟶ T. (¬(∀i:ℕ. ((f (i + 1)) < (f i))))
Definitions occuring in Statement :
nat: ℕ,
infix_ap: x f y,
all: ∀x:A. B[x],
not: ¬A,
apply: f a,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
function: x:A ⟶ B[x],
not: ¬A,
all: ∀x:A. B[x],
nat: ℕ,
infix_ap: x f y,
add: n + m,
natural_number: $n,
apply: f a
FDL editor aliases :
DCC
Latex:
DCC(T;<) == \mforall{}f:\mBbbN{} {}\mrightarrow{} T. (\mneg{}(\mforall{}i:\mBbbN{}. ((f (i + 1)) < (f i))))
Date html generated:
2016_07_08-PM-05_02_03
Last ObjectModification:
2015_09_23-AM-07_46_52
Theory : general
Home
Index