Re: [isabelle] Unnecessary assumption in HOL-Analysis.Convex.convex_on_alt



Great idea. Thanks!
Larry

> On 5 Oct 2020, at 14:02, Jakub Kądziołka <kuba at kadziolka.net> wrote:
> 
> Hello,
> 
> I have stumbled upon this lemma in HOL-Analysis.Convex:
> 
> lemma convex_on_alt:
> fixes C :: "'a::real_vector set"
> assumes "convex C"
> shows "convex_on C f ⟷
> (∀x ∈ C. ∀ y ∈ C. ∀ μ :: real. μ ≥ 0 ∧ μ ≤ 1 ⟶
> f (μ *⇩R x + (1 - μ) *⇩R y) ≤ μ * f x + (1 - μ) * f y)"
> 
> As this is a simple restatement of convex_on_def, I was somewhat puzzled
> by the assumption of "convex C". As it turns out - it's not necessary.
> I removed the assumes line and the proof succeeded without any
> modification. I suppose it would be useful to reflect this in the
> distribution?





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