Nuprl Definition : strongwellfounded
SWellFounded(R[x; y]) == ∃f:T ⟶ ℕ. ∀x,y:T. (R[x; y] ⇒ f x < f y)
Definitions occuring in Statement :
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
nat: ℕ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
less_than: a < b,
apply: f a
FDL editor aliases :
strongwellfounded
Latex:
SWellFounded(R[x; y]) == \mexists{}f:T {}\mrightarrow{} \mBbbN{}. \mforall{}x,y:T. (R[x; y] {}\mRightarrow{} f x < f y)
Date html generated:
2016_05_14-PM-03_52_10
Last ObjectModification:
2015_09_22-PM-06_01_47
Theory : relations2
Home
Index