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

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.


On Mon, Jun 6, 2016 at 7:04 AM, Jonathan Woodgate via Cl-isabelle-users <
cl-isabelle-users at> 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.