Topological properties of the set of convex/concave functions

We prove the following facts:

• isClosed_setOfPred_convexOn : the set of convex functions on a set is closed
• isClosed_setOfPred_concaveOn : the set of concave functions on a set is closed

theorem isClosed_setOfPred_convexOn {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [PartialOrder β] [TopologicalSpace β] [OrderClosedTopology β] [AddCommMonoid α] [AddCommMonoid β] [SMul 𝕜 α] [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] [ContinuousAdd β] {s : Set α} : IsClosed {f : α → β | ConvexOn 𝕜 s f}

The set of convex functions on a set s is closed.

@[deprecated isClosed_setOfPred_convexOn (since := "2026-07-09")]

theorem isClosed_setOf_convexOn {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [PartialOrder β] [TopologicalSpace β] [OrderClosedTopology β] [AddCommMonoid α] [AddCommMonoid β] [SMul 𝕜 α] [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] [ContinuousAdd β] {s : Set α} : IsClosed {f : α → β | ConvexOn 𝕜 s f}

Alias of isClosed_setOfPred_convexOn.

---

The set of convex functions on a set s is closed.

theorem isClosed_setOfPred_concaveOn {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [PartialOrder β] [TopologicalSpace β] [OrderClosedTopology β] [AddCommMonoid α] [AddCommMonoid β] [SMul 𝕜 α] [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] [ContinuousAdd β] {s : Set α} : IsClosed {f : α → β | ConcaveOn 𝕜 s f}

The set of concave functions on a set s is closed.

@[deprecated isClosed_setOfPred_concaveOn (since := "2026-07-09")]

theorem isClosed_setOf_concaveOn {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [PartialOrder β] [TopologicalSpace β] [OrderClosedTopology β] [AddCommMonoid α] [AddCommMonoid β] [SMul 𝕜 α] [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] [ContinuousAdd β] {s : Set α} : IsClosed {f : α → β | ConcaveOn 𝕜 s f}

Alias of isClosed_setOfPred_concaveOn.

---

The set of concave functions on a set s is closed.