Time 
Nick 
Message 
01:49 

ilbot3 joined #isabelle 
01:49 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
08:05 

dave24 joined #isabelle 
11:42 

ertes joined #isabelle 
12:20 
inte 
pruvisto: fwiw, the link to the Totient theory worked for me (and I'm not logged into bitbucket atm). 
12:30 
pruvisto 
inte: yes I changed the visibility by now 
12:30 
pruvisto 
it was set to "private" at first for some reason 
12:30 
pruvisto 
I switched it to "public" then but it still didn't work 
12:30 
inte 
ah. 
12:30 
pruvisto 
but after an hour or so, it finally worked 
12:30 
pruvisto 
apparently there's a bit of a delay there 
12:30 
inte 
gotta love caching 
12:47 

dmiles joined #isabelle 
12:49 

dmiles joined #isabelle 
15:57 

ertes joined #isabelle 
22:05 
chindy 
i should probably have paid more attention in linear algebra, but does this lemma hold? lemma "(P::real^2) > 0 ⟹ P ∙ A > P ∙ B ⟹ A > B" 
22:06 
inte 
well, what if all entries in P are equal 
22:07 
inte 
actually, hmm 
22:07 
chindy 
what then ? 
22:07 
inte 
what's ∙ here? 
22:07 
chindy 
dot product 
22:08 
inte 
okay then. let's pick P = (1,1), A = (2,0), B = (0,1) 
22:09 
chindy 
ah... im an idiot 
22:09 
chindy 
:P 
22:10 
inte 
let me guess, > is not a total order :) 
22:10 
chindy 
yea 
22:22 
chindy 
inte: what about ∃i . A$i > B$i instead of A > B ? 
22:37 

ertes joined #isabelle 
22:43 
inte 
well, that's the negation of !i. A$i <= B$i, and A <= B and P > 0 implies P \cdot A <= P \cdot B... so that should work fine. 