Time 
Nick 
Message 
00:04 
JCaesar 
yes, am indeed misunderstanding it… 
00:15 
chindy 
pruvisto: if i understand correctly shouldnt this lemma follow quite easily : lemma "setdist A B = 0 ==> \exist x : A . x : B" 
00:16 
chindy 
given that A and B are non empty 
03:05 

hazyPurple_ joined #isabelle 
05:12 

hazyPurple_ joined #isabelle 
07:31 

ertes joined #isabelle 
07:32 

ertes joined #isabelle 
07:49 
pruvisto 
chindy: no 
07:50 
pruvisto 
first of all, "∃x∈A. x ∈ B" can be written more idiomatically as "A ∩ B ≠ {}" 
07:51 
pruvisto 
second, consider "setdist 1 (ball 0 1)" 
07:51 
pruvisto 
or more generally, any point on the frontier of an open set 
07:51 
pruvisto 
er 
07:51 
pruvisto 
"setdist {1} (ball 0 1)", of course 
08:00 

dave24 joined #isabelle 
08:41 
JCaesar 
Btw, is there some type class for infinite types? 
10:50 

hazyPurple_ joined #isabelle 
11:00 

dmiles joined #isabelle 
11:02 

dmiles joined #isabelle 
11:45 
pruvisto 
chindy: you may find the lemma setdist_eq_0_closed interesting 
11:45 
pruvisto 
or setdist_eq_0_closed_compact 
11:46 
pruvisto 
oh, there's also "closest_point" 
15:57 

hazyPurple_ joined #isabelle 