theorem
Convex.quasiconvexOn_iSup
{𝕜 : Type u}
{E : Type v}
{β : Type w}
[Semiring 𝕜]
[PartialOrder 𝕜]
[AddCommMonoid E]
[SMul 𝕜 E]
[CompleteLattice β]
{s : Set E}
{I : Type x}
{f : I → E → β}
(hs : Convex 𝕜 s)
(hf : ∀ (i : I), QuasiconvexOn 𝕜 s (f i))
:
QuasiconvexOn 𝕜 s fun (x : E) => ⨆ (i : I), f i x
On a convex set, the pointwise supremum of a family of quasiconvex functions is quasiconvex.
theorem
quasiconvexOn_univ_iSup
{𝕜 : Type u}
{E : Type v}
{β : Type w}
[Semiring 𝕜]
[PartialOrder 𝕜]
[AddCommMonoid E]
[SMul 𝕜 E]
[CompleteLattice β]
{I : Type x}
{f : I → E → β}
(hf : ∀ (i : I), QuasiconvexOn 𝕜 Set.univ (f i))
:
QuasiconvexOn 𝕜 Set.univ fun (x : E) => ⨆ (i : I), f i x
Proposition 10.24: the pointwise supremum of a family of quasiconvex functions is
quasiconvex on the whole space. The textbook extended-real-valued real-vector-space statement is
the specialization 𝕜 = ℝ and β = EReal.