Nuprl Definition : no-descending-chain
no-descending-chain(T;<) == ∀f:ℕ ⟶ T. ∃j:ℕ. ∃i:ℕj. (¬((f j) < (f i)))
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
infix_ap: x f y,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
nat: ℕ,
exists: ∃x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
not: ¬A,
infix_ap: x f y,
apply: f a
FDL editor aliases :
no-descending-chain
Latex:
no-descending-chain(T;<) == \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mexists{}j:\mBbbN{}. \mexists{}i:\mBbbN{}j. (\mneg{}((f j) < (f i)))
Date html generated:
2016_05_13-PM-03_52_02
Last ObjectModification:
2015_09_22-PM-05_45_26
Theory : bar-induction
Home
Index