QuasiconcaveOn.dual

theorem QuasiconcaveOn.dual : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : LE β] [inst_3 : SMul 𝕜 E] {s : Set E} {f : E → β}, QuasiconcaveOn 𝕜 s f → QuasiconvexOn 𝕜 s (⇑OrderDual.toDual ∘ f)

This theorem states that for any ordered semiring `𝕜`, any additively commutative monoid `E`, any set `s` of elements from `E`, any function `f` from `E` to a type `β` equipped with a less-than-or-equal-to (`LE`) relation, and any scalar multiplication (`SMul`) between `𝕜` and `E`, if the function `f` is quasiconcave on the set `s` (meaning that all its superlevel sets are `𝕜`-convex), then the function `f`, when composed with the identity function to the order-dual of `β` (i.e., `f` considered in the opposite order), is quasiconvex on the set `s` (meaning that all its sublevel sets are `𝕜`-convex). In other words, the order-dual of a quasiconcave function is quasiconvex.

More concisely: The order-dual of a quasiconcave function defined on an ordered semiring and an additively commutative monoid is quasiconvex.