Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-04-20

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

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

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary