Theorems · Theorem · convex and discrete geometry
convex_Icc
∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
[inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : Module 𝕜 β] [PosSMulMono 𝕜 β] (r s : β),
Convex 𝕜 (Set.Icc r s)- Defined in
- Mathlib.Analysis.Convex.Basic
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- PartialOrderstatement and proof · cited by 6,410
- Set.Iccstatement · cited by 1,702
- IsOrderedAddMonoidstatement and proof · cited by 1,659
- Convexstatement · cited by 551
- PosSMulMonostatement and proof · cited by 188
- convex_Iciproof · cited by 29
- Convex.interproof · cited by 22
- Set.Ici_inter_Iicproof · cited by 12
- convex_Iicproof · cited by 12
Cited by29
Results whose statement or proof uses this declaration.
- uniqueDiffOn_Iccproof · cited by 21
- convex_uIccproof · cited by 5
- Real.abs_log_sub_add_sum_range_leproof · cited by 4
- IsMinOn.of_isLocalMinOn_of_convexOnproof · cited by 2
- AkraBazziRecurrence.isBigO_apply_r_sub_bproof · cited by 2
- strictConcaveOn_sin_Iccproof · cited by 2
- MeasureTheory.integrableOn_Icc_deriv_smul_iff_of_deriv_nonposproof · cited by 1
- Real.qaryEntropy_strictAntiOnproof · cited by 1
- Real.qaryEntropy_strictMonoOnproof · cited by 1
- Real.strictConcaveOn_qaryEntropyproof · cited by 1
- Real.sum_range_le_log_divproof · cited by 1
- Real.sum_range_sub_log_div_leproof · cited by 1