Time Nick Message
00:38 chindy is there a standard way of limiting the set real to all reals >0 ?
07:13 pruvisto chindy: {x. x > 0}
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:08 int-e UNIV :: real set is the set of all real numbers.
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