Re: [isabelle] the minimum of a set

Hi Paqui,

> I have defined i = Min {x. P(x)}. 
> Next, I try to prove that P(i) holds or even that  i\<in> Min {x. P(x)} and
> I cannot neither "by auto", nor "by (auto! simp add: Min_def)", 
> nor "by (auto! simp add: Min_in)", .

The issue is that {x. P(x)} might be the empty set, in which case Min
{x. P(x)} is unspecified.   Inspect theorems Min_Un Min_insert
Min_singleton to get an idea how you might proceed from the definition

Hope this helps


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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