[isabelle] the minimum of a set


In a proof in Isabelle/HOL, 

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)", .

Please, some help?,



Paqui Lucio

Basque Country University




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