Stream: Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Oct 06 2020 at 09:03):

From: Jakub Kądziołka <kuba@kadziolka.net>
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?

Kind regards,
Jakub Kądziołka


Last updated: Sep 28 2021 at 19:14 UTC