Re: [isabelle] Set Comprehention {5n. nâN} without existence-quantor?



Thank you! 

    Mario Carneiro <di.gama at gmail.com> schrieb am 13:20 Montag, 6.Juni 2016:
 

 Yes, that is the ideal (5), which is the smallest ideal containing 5. I
don't know the Isabelle notation, but that would be something like

{n. forall i in Ideals(N), 5 in i => n in i}

where i in Ideals(N) if ax+b in i whenever a,b in i and x in N.

Mario

On Mon, Jun 6, 2016 at 7:04 AM, Jonathan Woodgate via Cl-isabelle-users <
cl-isabelle-users at lists.cam.ac.uk> wrote:

> Hello,
> is there any alternative way of writing {5n.nâN} other than {k. \ex n. k =
> 5n}..such as using with "forAll" operator or so (thus avoiding the
> existence-quantor?)
> Thank you!
>
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.