Theorems · Definition · convex and discrete geometry
QuasiconcaveOn
(𝕜 : Type u_1) →
{E : Type u_2} →
{β : Type u_3} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [LE β] → [SMul 𝕜 E] → Set E → (E → β) → PropA function is quasiconcave if all its superlevels are convex.
This means that, for all r, {x ∈ s | r ≤ f x} is 𝕜-convex.
- Defined in
- Mathlib.Analysis.Convex.Quasiconvex
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- PartialOrderstatement and proof · cited by 6,410
- Set.ofPredproof · cited by 6,101
- Convexproof · cited by 551
Cited by27
Results whose statement or proof uses this declaration.
- QuasilinearOnproof · cited by 11
- QuasiconcaveOn.dualstatement · cited by 3
- Sion.minimaxstatement and proof · cited by 2
- MonotoneOn.quasiconcaveOnstatement · cited by 2
- QuasiconcaveOn.monotone_compstatement and proof · cited by 2
- AntitoneOn.quasiconcaveOnstatement · cited by 2
- Antitone.quasiconcaveOnstatement · cited by 1
- quasiconcaveOn_iff_min_lestatement · cited by 1
- Monotone.quasiconcaveOnstatement · cited by 1
- Sion.DMCompletion.exists_isSaddlePointOnstatement and proof · cited by 1
- Sion.exists_isSaddlePointOn'statement and proof · cited by 1
- Sion.exists_lt_iInf_of_lt_iInf_of_finitestatement and proof · cited by 1