Commit 2023-08-14 12:56 6b723c04

View on Github →

chore: quasiconvexity doesn't need an additive structure on the codomain (#6494)

Estimated changes

Modified Mathlib/Analysis/Convex/Quasiconvex.lean

modified theorem QuasiconcaveOn.inf

modified theorem QuasiconvexOn.sup

modified theorem QuasilinearOn.monotoneOn_or_antitoneOn

modified theorem quasilinearOn_iff_monotoneOn_or_antitoneOn