2025/04/04

Newest at the top

2025-04-04 17:51:38 +0200amadaluzia(~amadaluzi@user/amadaluzia) (Ping timeout: 245 seconds)
2025-04-04 17:51:32 +0200 <EvanR> nope
2025-04-04 17:51:20 +0200 <kuribas> The formula?
2025-04-04 17:51:14 +0200 <EvanR> what is
2025-04-04 17:49:57 +0200 <kuribas> It's easy for naturals no?
2025-04-04 17:49:35 +0200rit(~rit@2409:40e0:39:317c:5ce4:875:e0a7:d628)
2025-04-04 17:48:39 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 252 seconds)
2025-04-04 17:47:19 +0200 <EvanR> immediately
2025-04-04 17:46:49 +0200 <kuribas> Where do you get stuck?
2025-04-04 17:46:35 +0200 <EvanR> oh this is the same question. Well I tried that too and couldn't figure it out
2025-04-04 17:45:59 +0200 <EvanR> nvm
2025-04-04 17:45:53 +0200 <EvanR> wait
2025-04-04 17:45:50 +0200 <EvanR> just cancel 4 things?
2025-04-04 17:45:39 +0200 <EvanR> if aaa / (bbb) < ccc / (ddd) then a/b < c/d?
2025-04-04 17:43:30 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-04-04 17:42:26 +0200L29Ah(~L29Ah@wikipedia/L29Ah) (Ping timeout: 252 seconds)
2025-04-04 17:41:52 +0200 <kuribas> For integral values of a, b, c, and d.
2025-04-04 17:41:40 +0200 <kuribas> You could prove that (a*a*a)/(b*b*b) < (c*c*c*)/(d*d*d) then a/b < c/d
2025-04-04 17:35:15 +0200 <EvanR> that means I don't have to solve this using the "hint use an indirect proof": Show that family of intervals [a,b] where a^3 <= 2 and 2 <= b^3 is consistent (any interval in the family intersects all the others)
2025-04-04 17:32:39 +0200 <EvanR> cool
2025-04-04 17:32:33 +0200 <EvanR> a < b? yes, then you're done. Or a == b, then a^3==b^3 contradicting a^3 < b^3. Or b < a, using the above, b^3 < a^3, also contradicting.
2025-04-04 17:25:14 +0200 <EvanR> somehow
2025-04-04 17:24:24 +0200 <EvanR> maybe in chapter 17 there will be a thing to prove that any monotonic functions on reals can be downgraded to a monotonic function on rationals
2025-04-04 17:24:00 +0200fp1(~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 272 seconds)
2025-04-04 17:22:15 +0200 <EvanR> again, the task to is to reason from what's assumed and not from "any argument whatever"
2025-04-04 17:21:51 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 276 seconds)
2025-04-04 17:21:46 +0200 <EvanR> so I can't solve chapter 1 by using chapter 17 from the other book
2025-04-04 17:21:38 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-04 17:21:30 +0200 <EvanR> this is "real anaylsis: a constructive approach"
2025-04-04 17:21:29 +0200 <int-e> (another fact)
2025-04-04 17:21:10 +0200 <int-e> the rationals are a subfield of the reals
2025-04-04 17:20:56 +0200 <EvanR> also it wouldn't even help, are you going to apply a function coded for real numbers to rationals? xD
2025-04-04 17:20:28 +0200notdabs(~Owner@2600:1700:69cf:9000:c0fa:b50a:3031:4dce) (Quit: Leaving)
2025-04-04 17:20:04 +0200 <EvanR> I didn't that's the point
2025-04-04 17:19:56 +0200 <EvanR> but we just proved that
2025-04-04 17:19:56 +0200 <int-e> so how did you get there for the cube root in the reals?
2025-04-04 17:19:36 +0200 <EvanR> it might be but I didn't get there
2025-04-04 17:19:05 +0200int-eshrugs
2025-04-04 17:19:05 +0200 <EvanR> not absolute truths, or "doesn't matter somebody somewhere has already done this one"
2025-04-04 17:18:58 +0200 <int-e> well, f(x) = x^3 being monotonic is a fact about rational number.s
2025-04-04 17:18:32 +0200 <EvanR> I don't understand, I'm not skeptical. I'm trying to go from certain assumptions to a conclusion
2025-04-04 17:16:47 +0200 <int-e> well it's not if you apply the same level of skepticism that you're currently applying to the strict monotonicity of f(x) = x^3 in the rationals
2025-04-04 17:16:12 +0200 <EvanR> well that's a fact about real numbers right
2025-04-04 17:16:08 +0200__jmcantrell__(~weechat@user/jmcantrell) jmcantrell
2025-04-04 17:15:31 +0200 <int-e> TBH the funny part of this is that you were (apparently) willing to accept that the cube root function is strictly monotonic.
2025-04-04 17:13:34 +0200dolio(~dolio@130.44.140.168) dolio
2025-04-04 17:13:18 +0200rit(~rit@2409:40e0:39:317c:5ce4:875:e0a7:d628) (Remote host closed the connection)
2025-04-04 17:13:03 +0200EvanRrecapitulates
2025-04-04 17:12:35 +0200 <EvanR> er
2025-04-04 17:12:30 +0200dolio(~dolio@130.44.140.168) (Client Quit)