News for hackers. Stuff that matters.

A comment on Now I’m calculating with constructive reals. Parent comment

Re:Now I’m calculating with constructive reals by jonsen on Wednesday April 27, 2022 @03:00PM (#31184306)
Yes, but your argument goes circular with this. And someone could argue that

  .999.../2 = .499...  <=>  .999... = 2*.499... = .499...+.499...
which "surely must" have 8 as the rightmost digit. Moving it further away from 1.
[ Parent | on HN ]
Re:Now I’m calculating with constructive reals by peterhalburt33 on Wednesday April 27, 2022 @04:44PM (#31185552)
Agreed this isn’t airtight, but if you accept the premise that real numbers are specified by their sequence decimal digits: .499…+.499… has 9 as its first digit after the decimal, 9 as its second and so on - the only other number that has this decimal expansion is .999… infinitely repeating, so these must be the same numbers.
[ Parent | on HN ]