# IRC log for #isabelle, 2017-03-21

All times shown according to UTC.

Time Nick Message
00:38 chindy is there a standard way of limiting the set real to all reals >0 ?
02:47 ilbot3 joined #isabelle
02:47 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/
07:13 pruvisto chindy: {x. x > 0}
11:36 silver joined #isabelle
12:01 cic joined #isabelle
15:36 ammbauer joined #isabelle
17:26 chindy how do i specify a set of all elements of type: For example for showing total_on as an example:  "total_on_nat Rel â· (total_on (Nats::nat) (Rel:: nat * nat))". where i intend to show that Rel is total on Natural numbers
17:47 ammbauer chindy: use UNIV.
17:47 ammbauer "total_on_nat Rel <--> total_on UNIV (Rel::nat rel)"
17:47 ammbauer or with fancy abbreviation "total_on_nat Rel <--> total (Rel::nat rel)"
18:06 chindy so "let s = UNIV (X::real set) in" .... lets s be a set of all elements e taht are element of real ?
18:07 silver_ joined #isabelle
18:08 int-e UNIV :: real set  is the set of all real numbers.
18:11 ertesx joined #isabelle
18:12 int-e note: lemma "{x. True} = UNIV" by simp
18:19 chindy ah thx
20:47 JCaesar btw, the statement 'element of real' doesn't really make sense in Isabelle/HOLâ¦
20:48 pruvisto Well, there is the constant "â", which is the set of all real numbers
20:49 pruvisto but it only makes sense as a subset of a real algebra
20:49 pruvisto e.g. you can have "â :: complex"
20:49 pruvisto the set of all real numbers, viewed as a subset of the complex numbers
21:22 chindy pruvisto: thanks, but I think in my case it made sense as i had a (real, real) set and needed it to be total, which needs a set so "total_on (UNIV :: real set) relation" is probably the way to go
21:52 wagle joined #isabelle
23:35 stoopkid joined #isabelle