Nuprl Definition : fixedpoint-property
FP(X) == ∀f:FUN(X ⟶ X). ∀n:ℕ+. ∃x:X. (mdist(d;f x;x) ≤ (r1/r(n)))
Definitions occuring in Statement :
mfun: FUN(X ⟶ Y),
mdist: mdist(d;x;y),
rdiv: (x/y),
rleq: x ≤ y,
int-to-real: r(n),
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
natural_number: $n
FDL editor aliases :
fixedpoint-property
Latex:
FP(X) == \mforall{}f:FUN(X {}\mrightarrow{} X). \mforall{}n:\mBbbN{}\msupplus{}. \mexists{}x:X. (mdist(d;f x;x) \mleq{} (r1/r(n)))
Date html generated:
2020_05_20-AM-11_53_18
Last ObjectModification:
2019_11_20-PM-01_58_02
Theory : reals
Home
Index