Documentation Verification Report

Function

📁 Source: Mathlib/Analysis/Convex/Function.lean

Statistics

MetricCount
DefinitionsConcaveOn, ConvexOn, StrictConcaveOn, StrictConvexOn
4
Theoremsadd, add_const, add_strictConcaveOn, comp, comp_affineMap, comp_convexOn, comp_linearMap, convex_ge, convex_gt, convex_hypograph, convex_strict_hypograph, dual, ge_on_segment, ge_on_segment', inf, left_le_of_le_right, left_le_of_le_right', left_le_of_le_right'', left_lt_of_lt_right, left_lt_of_lt_right', lt_right_of_left_lt, lt_right_of_left_lt', neg, openSegment_subset_strict_hypograph, right_le_of_le_left, right_le_of_le_left', right_le_of_le_left'', smul, sub, sub_strictConvexOn, subset, translate_left, translate_right, add, add_const, add_strictConvexOn, comp, comp_affineMap, comp_concaveOn, comp_linearMap, convex_epigraph, convex_le, convex_lt, convex_strict_epigraph, dual, le_left_of_right_le, le_left_of_right_le', le_left_of_right_le'', le_on_segment, le_on_segment', le_right_of_left_le, le_right_of_left_le', le_right_of_left_le'', lt_left_of_right_lt, lt_left_of_right_lt', lt_right_of_left_lt, lt_right_of_left_lt', neg, openSegment_subset_strict_epigraph, smul, sub, sub_strictConcaveOn, subset, sup, translate_left, translate_right, concaveOn, convexOn, concaveOn_of_lt, convexOn_of_lt, strictConcaveOn_of_lt, strictConvexOn_of_lt, concaveOn_symm, convexOn_symm, strictConcaveOn_symm, strictConvexOn_symm, add, add_concaveOn, add_const, comp, comp_strictConvexOn, concaveOn, convex_gt, dual, eq_of_isMaxOn, inf, lt_on_openSegment, lt_on_open_segment', neg, sub, sub_convexOn, subset, translate_left, translate_right, add, add_const, add_convexOn, comp, comp_strictConcaveOn, convexOn, convex_lt, dual, eq_of_isMinOn, lt_on_openSegment, lt_on_open_segment', neg, sub, sub_concaveOn, subset, sup, translate_left, translate_right, concaveOn_const, concaveOn_id, concaveOn_iff_convex_hypograph, concaveOn_iff_div, concaveOn_iff_forall_pos, concaveOn_iff_pairwise_pos, concaveOn_of_convex_hypograph, convexOn_const, convexOn_id, convexOn_iff_convex_epigraph, convexOn_iff_div, convexOn_iff_forall_pos, convexOn_iff_pairwise_pos, convexOn_of_convex_epigraph, neg_concaveOn_iff, neg_convexOn_iff, neg_strictConcaveOn_iff, neg_strictConvexOn_iff, strictConcaveOn_iff_div, strictConvexOn_iff_div
132
Total136

ConcaveOn

Theorems

NameKindAssumesProvesValidatesDepends On
add 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConvexOn.add
OrderDual.isOrderedAddMonoid
dual
add_const 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add
concaveOn_const
add_strictConcaveOn 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
StrictConcaveOn
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConvexOn.add_strictConvexOn
OrderDual.isOrderedAddCancelMonoid
dual
StrictConcaveOn.dual
comp 📖ConcaveOn
Set.image
MonotoneOn
PartialOrder.toPreorder
LE.le.trans
Set.mem_image_of_mem
comp_affineMap 📖mathematicalConcaveOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
DFunLike.coe
AffineMap
DivisionRing.toRing
Field.toDivisionRing
addGroupIsAddTorsor
AffineMap.instFunLike
ConvexOn.comp_affineMap
dual
comp_convexOn 📖ConcaveOn
Set.image
ConvexOn
AntitoneOn
PartialOrder.toPreorder
ConvexOn.comp
dual
comp_linearMap 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
DFunLike.coe
LinearMap
RingHom.id
Semiring.toNonAssocSemiring
LinearMap.instFunLike
ConvexOn.comp_linearMap
dual
convex_ge 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
setOf
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
ConvexOn.convex_le
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulMono
dual
convex_gt 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
setOf
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
ConvexOn.convex_lt
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
convex_hypograph 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
Prod.instAddCommMonoid
Prod.instSMul
setOf
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
ConvexOn.convex_epigraph
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulMono
dual
convex_strict_hypograph 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
Prod.instAddCommMonoid
Prod.instSMul
setOf
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
ConvexOn.convex_strict_epigraph
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
dual 📖mathematicalConcaveOnConvexOn
OrderDual
OrderDual.instAddCommMonoid
OrderDual.instPartialOrder
OrderDual.instSMul
DFunLike.coe
Equiv
EquivLike.toFunLike
Equiv.instEquivLike
OrderDual.toDual
ge_on_segment 📖mathematicalConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
segment
Preorder.toLE
PartialOrder.toPreorder
SemilatticeInf.toMin
ConvexOn.le_on_segment
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulStrictMono
dual
ge_on_segment' 📖mathematicalConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
SemilatticeInf.toMin
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConvexOn.le_on_segment'
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulStrictMono
dual
inf 📖mathematicalConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instMinForall_mathlib
SemilatticeInf.toMin
ConvexOn.sup
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulStrictMono
dual
left_le_of_le_right 📖ConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
openSegment
Preorder.toLE
PartialOrder.toPreorder
ConvexOn.le_left_of_right_le
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
left_le_of_le_right' 📖ConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Preorder.toLE
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConvexOn.le_left_of_right_le'
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
left_le_of_le_right'' 📖ConcaveOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
NonUnitalNonAssocSemiring.toAddCommMonoid
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
NonUnitalCommRing.toNonUnitalNonAssocCommRing
CommRing.toNonUnitalCommRing
Field.toCommRing
Algebra.toSMul
Semifield.toCommSemiring
CommSemiring.toSemiring
Algebra.id
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
Preorder.toLT
ConvexOn.le_left_of_right_le''
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
left_lt_of_lt_right 📖ConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
openSegment
Preorder.toLT
PartialOrder.toPreorder
ConvexOn.lt_left_of_right_lt
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
left_lt_of_lt_right' 📖ConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConvexOn.lt_left_of_right_lt'
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
lt_right_of_left_lt 📖ConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
openSegment
Preorder.toLT
PartialOrder.toPreorder
ConvexOn.lt_right_of_left_lt
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
lt_right_of_left_lt' 📖ConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConvexOn.lt_right_of_left_lt'
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
neg 📖mathematicalConcaveOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConvexOn
Pi.instNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
neg_convexOn_iff
openSegment_subset_strict_hypograph 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
Preorder.toLE
Set.instHasSubset
openSegment
Prod.instAddCommMonoid
Prod.instSMul
setOf
ConvexOn.openSegment_subset_strict_epigraph
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
right_le_of_le_left 📖ConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
openSegment
Preorder.toLE
PartialOrder.toPreorder
ConvexOn.le_right_of_left_le
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
right_le_of_le_left' 📖ConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Preorder.toLT
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConvexOn.le_right_of_left_le'
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
right_le_of_le_left'' 📖ConcaveOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
NonUnitalNonAssocSemiring.toAddCommMonoid
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
NonUnitalCommRing.toNonUnitalNonAssocCommRing
CommRing.toNonUnitalCommRing
Field.toCommRing
Algebra.toSMul
Semifield.toCommSemiring
CommSemiring.toSemiring
Algebra.id
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
Preorder.toLE
ConvexOn.le_right_of_left_le''
OrderDual.isOrderedAddCancelMonoid
OrderDual.instPosSMulStrictMono
dual
smul 📖Preorder.toLE
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
CommSemiring.toSemiring
ConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConvexOn.smul
OrderDual.instPosSMulMono
dual
sub 📖mathematicalConcaveOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConvexOn
Pi.instSub
SubNegMonoid.toSub
add
ConvexOn.neg
sub_eq_add_neg
sub_strictConvexOn 📖mathematicalConcaveOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
StrictConvexOn
StrictConcaveOn
Pi.instSub
SubNegMonoid.toSub
add_strictConcaveOn
IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
StrictConvexOn.neg
sub_eq_add_neg
subset 📖ConcaveOn
Set
Set.instHasSubset
Convex
translate_left 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConvexOn.translate_left
dual
translate_right 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConvexOn.translate_right
dual

ConvexOn

Theorems

NameKindAssumesProvesValidatesDepends On
add 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add_le_add
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
smul_add
add_add_add_comm
add_const 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add
convexOn_const
add_strictConvexOn 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
StrictConvexOn
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
StrictConvexOn.add_convexOn
add_comm
comp 📖ConvexOn
Set.image
MonotoneOn
PartialOrder.toPreorder
LE.le.trans
Set.mem_image_of_mem
comp_affineMap 📖mathematicalConvexOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
DFunLike.coe
AffineMap
DivisionRing.toRing
Field.toDivisionRing
addGroupIsAddTorsor
AffineMap.instFunLike
Convex.affine_preimage
Convex.combo_affine_apply
comp_concaveOn 📖ConvexOn
Set.image
ConcaveOn
AntitoneOn
PartialOrder.toPreorder
ConcaveOn.comp
dual
comp_linearMap 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
DFunLike.coe
LinearMap
RingHom.id
Semiring.toNonAssocSemiring
LinearMap.instFunLike
Convex.linear_preimage
LinearMap.map_add
LinearMap.map_smul
convex_epigraph 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
Prod.instAddCommMonoid
Prod.instSMul
setOf
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
add_le_add
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
smul_le_smul_of_nonneg_left
convex_le 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
setOf
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
add_le_add
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
smul_le_smul_of_nonneg_left
Convex.combo_self
convex_lt 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
setOf
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
convex_iff_forall_pos
LT.lt.le
add_lt_add_of_lt_of_le
IsOrderedAddMonoid.toAddLeftMono
IsOrderedCancelAddMonoid.toIsOrderedAddMonoid
IsRightCancelAdd.addRightStrictMono_of_addRightMono
IsCancelAdd.toIsRightCancelAdd
IsOrderedCancelAddMonoid.toIsCancelAdd
covariant_swap_add_of_covariant_add
smul_lt_smul_of_pos_left
smul_le_smul_of_nonneg_left
PosSMulStrictMono.toPosSMulMono
Convex.combo_self
convex_strict_epigraph 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
Prod.instAddCommMonoid
Prod.instSMul
setOf
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
convex_iff_openSegment_subset
openSegment_subset_strict_epigraph
LT.lt.le
dual 📖mathematicalConvexOnConcaveOn
OrderDual
OrderDual.instAddCommMonoid
OrderDual.instPartialOrder
OrderDual.instSMul
DFunLike.coe
Equiv
EquivLike.toFunLike
Equiv.instEquivLike
OrderDual.toDual
le_left_of_right_le 📖ConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
openSegment
Preorder.toLE
PartialOrder.toPreorder
le_left_of_right_le'
LT.lt.le
le_left_of_right_le' 📖ConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Preorder.toLE
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
le_of_not_gt
lt_irrefl
LT.lt.le
add_lt_add_of_lt_of_le
IsOrderedAddMonoid.toAddLeftMono
IsOrderedCancelAddMonoid.toIsOrderedAddMonoid
IsRightCancelAdd.addRightStrictMono_of_addRightMono
IsCancelAdd.toIsRightCancelAdd
IsOrderedCancelAddMonoid.toIsCancelAdd
covariant_swap_add_of_covariant_add
smul_lt_smul_of_pos_left
smul_le_smul_of_nonneg_left
PosSMulStrictMono.toPosSMulMono
Convex.combo_self
le_left_of_right_le'' 📖ConvexOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
NonUnitalNonAssocSemiring.toAddCommMonoid
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
NonUnitalCommRing.toNonUnitalNonAssocCommRing
CommRing.toNonUnitalCommRing
Field.toCommRing
Algebra.toSMul
Semifield.toCommSemiring
CommSemiring.toSemiring
Algebra.id
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
Preorder.toLT
LE.le.eq_or_lt
Eq.ge
le_left_of_right_le
Ioo_subset_openSegment
le_on_segment 📖mathematicalConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
segment
Preorder.toLE
PartialOrder.toPreorder
SemilatticeSup.toMax
Lattice.toSemilatticeSup
le_on_segment'
le_on_segment' 📖mathematicalConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
SemilatticeSup.toMax
Lattice.toSemilatticeSup
add_le_add
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
smul_le_smul_of_nonneg_left
PosSMulStrictMono.toPosSMulMono
le_max_left
le_max_right
Convex.combo_self
le_right_of_left_le 📖ConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
openSegment
Preorder.toLE
PartialOrder.toPreorder
le_right_of_left_le'
LT.lt.le
le_right_of_left_le' 📖ConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Preorder.toLT
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add_comm
le_left_of_right_le'
le_right_of_left_le'' 📖ConvexOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
NonUnitalNonAssocSemiring.toAddCommMonoid
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
NonUnitalCommRing.toNonUnitalNonAssocCommRing
CommRing.toNonUnitalCommRing
Field.toCommRing
Algebra.toSMul
Semifield.toCommSemiring
CommSemiring.toSemiring
Algebra.id
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
Preorder.toLE
LE.le.eq_or_lt
Eq.le
le_right_of_left_le
Ioo_subset_openSegment
lt_left_of_right_lt 📖ConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
openSegment
Preorder.toLT
PartialOrder.toPreorder
lt_left_of_right_lt'
lt_left_of_right_lt' 📖ConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
not_le
lt_irrefl
LT.lt.le
add_lt_add_of_le_of_lt
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
IsCancelAdd.toIsLeftCancelAdd
IsOrderedCancelAddMonoid.toIsCancelAdd
IsOrderedAddMonoid.toAddLeftMono
IsOrderedCancelAddMonoid.toIsOrderedAddMonoid
covariant_swap_add_of_covariant_add
smul_le_smul_of_nonneg_left
PosSMulStrictMono.toPosSMulMono
smul_lt_smul_of_pos_left
Convex.combo_self
lt_right_of_left_lt 📖ConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
openSegment
Preorder.toLT
PartialOrder.toPreorder
lt_right_of_left_lt'
lt_right_of_left_lt' 📖ConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add_comm
lt_left_of_right_lt'
neg 📖mathematicalConvexOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConcaveOn
Pi.instNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
neg_concaveOn_iff
openSegment_subset_strict_epigraph 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
Preorder.toLE
Set.instHasSubset
openSegment
Prod.instAddCommMonoid
Prod.instSMul
setOf
LT.lt.le
add_lt_add_of_lt_of_le
IsOrderedAddMonoid.toAddLeftMono
IsOrderedCancelAddMonoid.toIsOrderedAddMonoid
IsRightCancelAdd.addRightStrictMono_of_addRightMono
IsCancelAdd.toIsRightCancelAdd
IsOrderedCancelAddMonoid.toIsCancelAdd
covariant_swap_add_of_covariant_add
smul_lt_smul_of_pos_left
smul_le_smul_of_nonneg_left
PosSMulStrictMono.toPosSMulMono
smul 📖Preorder.toLE
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
CommSemiring.toSemiring
ConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
smul_le_smul_of_nonneg_left
smul_add
SMulCommClass.smul_comm
smulCommClass_self
sub 📖mathematicalConvexOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConcaveOn
Pi.instSub
SubNegMonoid.toSub
add
ConcaveOn.neg
sub_eq_add_neg
sub_strictConcaveOn 📖mathematicalConvexOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
StrictConcaveOn
StrictConvexOn
Pi.instSub
SubNegMonoid.toSub
add_strictConvexOn
IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
StrictConcaveOn.neg
sub_eq_add_neg
subset 📖ConvexOn
Set
Set.instHasSubset
Convex
sup 📖mathematicalConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instMaxForall_mathlib
SemilatticeSup.toMax
Lattice.toSemilatticeSup
sup_le
add_le_add
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
smul_le_smul_of_nonneg_left
PosSMulStrictMono.toPosSMulMono
le_sup_left
le_sup_right
translate_left 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add_comm
translate_right
translate_right 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
Convex.translate_preimage_right
smul_add
add_add_add_comm
Convex.combo_self

LinearMap

Theorems

NameKindAssumesProvesValidatesDepends On
concaveOn 📖mathematicalConvex
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConcaveOn
DFunLike.coe
LinearMap
RingHom.id
Semiring.toNonAssocSemiring
instFunLike
map_add
map_smul
le_refl
convexOn 📖mathematicalConvex
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConvexOn
DFunLike.coe
LinearMap
RingHom.id
Semiring.toNonAssocSemiring
instFunLike
map_add
map_smul
le_refl

LinearOrder

Theorems

NameKindAssumesProvesValidatesDepends On
concaveOn_of_lt 📖mathematicalConvex
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Preorder.toLE
PartialOrder.toPreorder
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConcaveOnconvexOn_of_lt
convexOn_of_lt 📖mathematicalConvex
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Preorder.toLE
PartialOrder.toPreorder
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
ConvexOnconvexOn_iff_pairwise_pos
add_comm
Ne.lt_or_gt
strictConcaveOn_of_lt 📖mathematicalConvex
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Preorder.toLT
PartialOrder.toPreorder
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
StrictConcaveOnstrictConvexOn_of_lt
strictConvexOn_of_lt 📖mathematicalConvex
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Preorder.toLT
PartialOrder.toPreorder
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
StrictConvexOnadd_comm
Ne.lt_or_gt

OrderIso

Theorems

NameKindAssumesProvesValidatesDepends On
concaveOn_symm 📖mathematicalConvexOn
Set.univ
DFunLike.coe
OrderIso
Preorder.toLE
PartialOrder.toPreorder
instFunLikeOrderIso
ConcaveOn
symm
convex_univ
Function.Surjective.exists
surjective
symm_apply_apply
le_iff_le
apply_symm_apply
convexOn_symm 📖mathematicalConcaveOn
Set.univ
DFunLike.coe
OrderIso
Preorder.toLE
PartialOrder.toPreorder
instFunLikeOrderIso
ConvexOn
symm
convex_univ
Function.Surjective.exists
surjective
symm_apply_apply
le_iff_le
apply_symm_apply
strictConcaveOn_symm 📖mathematicalStrictConvexOn
Set.univ
DFunLike.coe
OrderIso
Preorder.toLE
PartialOrder.toPreorder
instFunLikeOrderIso
StrictConcaveOn
symm
convex_univ
Function.Surjective.exists
surjective
injective
symm_apply_apply
lt_iff_lt
apply_symm_apply
strictConvexOn_symm 📖mathematicalStrictConcaveOn
Set.univ
DFunLike.coe
OrderIso
Preorder.toLE
PartialOrder.toPreorder
instFunLikeOrderIso
StrictConvexOn
symm
convex_univ
Function.Surjective.exists
surjective
injective
symm_apply_apply
lt_iff_lt
apply_symm_apply

StrictConcaveOn

Theorems

NameKindAssumesProvesValidatesDepends On
add 📖mathematicalStrictConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
StrictConvexOn.add
OrderDual.isOrderedAddCancelMonoid
dual
add_concaveOn 📖mathematicalStrictConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
ConcaveOn
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
StrictConvexOn.add_convexOn
OrderDual.isOrderedAddCancelMonoid
dual
ConcaveOn.dual
add_const 📖mathematicalStrictConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add_concaveOn
concaveOn_const
comp 📖StrictConcaveOn
Set.image
StrictMonoOn
PartialOrder.toPreorder
Set.InjOn
LT.lt.trans
Set.mem_image_of_mem
LT.lt.le
comp_strictConvexOn 📖StrictConcaveOn
Set.image
StrictConvexOn
StrictAntiOn
PartialOrder.toPreorder
Set.InjOn
StrictConvexOn.comp
dual
concaveOn 📖mathematicalStrictConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConcaveOnStrictConvexOn.convexOn
dual
convex_gt 📖mathematicalStrictConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
setOf
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
StrictConvexOn.convex_lt
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulMono
dual
dual 📖mathematicalStrictConcaveOnStrictConvexOn
OrderDual
OrderDual.instAddCommMonoid
OrderDual.instPartialOrder
OrderDual.instSMul
DFunLike.coe
Equiv
EquivLike.toFunLike
Equiv.instEquivLike
OrderDual.toDual
eq_of_isMaxOn 📖StrictConcaveOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
IsMaxOn
PartialOrder.toPreorder
Set
Set.instMembership
StrictConvexOn.eq_of_isMinOn
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulMono
dual
inf 📖mathematicalStrictConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instMinForall_mathlib
SemilatticeInf.toMin
StrictConvexOn.sup
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulStrictMono
dual
lt_on_openSegment 📖mathematicalStrictConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
openSegment
Preorder.toLT
PartialOrder.toPreorder
SemilatticeInf.toMin
StrictConvexOn.lt_on_openSegment
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulStrictMono
dual
lt_on_open_segment' 📖mathematicalStrictConcaveOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
SemilatticeInf.toMin
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
StrictConvexOn.lt_on_open_segment'
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulStrictMono
dual
neg 📖mathematicalStrictConcaveOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
StrictConvexOn
Pi.instNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
neg_strictConvexOn_iff
sub 📖mathematicalStrictConcaveOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
StrictConvexOn
Pi.instSub
SubNegMonoid.toSub
add
IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
StrictConvexOn.neg
sub_eq_add_neg
sub_convexOn 📖mathematicalStrictConcaveOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConvexOn
Pi.instSub
SubNegMonoid.toSub
add_concaveOn
IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
ConvexOn.neg
sub_eq_add_neg
subset 📖StrictConcaveOn
Set
Set.instHasSubset
Convex
translate_left 📖mathematicalStrictConcaveOn
AddCancelCommMonoid.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add_comm
translate_right
translate_right 📖mathematicalStrictConcaveOn
AddCancelCommMonoid.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
StrictConvexOn.translate_right
dual

StrictConvexOn

Theorems

NameKindAssumesProvesValidatesDepends On
add 📖mathematicalStrictConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add_lt_add
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
IsCancelAdd.toIsLeftCancelAdd
IsOrderedCancelAddMonoid.toIsCancelAdd
IsOrderedAddMonoid.toAddLeftMono
IsOrderedCancelAddMonoid.toIsOrderedAddMonoid
IsRightCancelAdd.addRightStrictMono_of_addRightMono
IsCancelAdd.toIsRightCancelAdd
covariant_swap_add_of_covariant_add
smul_add
add_add_add_comm
add_const 📖mathematicalStrictConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add_convexOn
convexOn_const
add_convexOn 📖mathematicalStrictConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
ConvexOn
Pi.instAdd
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add_lt_add_of_lt_of_le
IsOrderedAddMonoid.toAddLeftMono
IsOrderedCancelAddMonoid.toIsOrderedAddMonoid
IsRightCancelAdd.addRightStrictMono_of_addRightMono
IsCancelAdd.toIsRightCancelAdd
IsOrderedCancelAddMonoid.toIsCancelAdd
covariant_swap_add_of_covariant_add
LT.lt.le
smul_add
add_add_add_comm
comp 📖StrictConvexOn
Set.image
StrictMonoOn
PartialOrder.toPreorder
Set.InjOn
LT.lt.trans
Set.mem_image_of_mem
LT.lt.le
comp_strictConcaveOn 📖StrictConvexOn
Set.image
StrictConcaveOn
StrictAntiOn
PartialOrder.toPreorder
Set.InjOn
StrictConcaveOn.comp
dual
convexOn 📖mathematicalStrictConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConvexOnconvexOn_iff_pairwise_pos
LT.lt.le
convex_lt 📖mathematicalStrictConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
setOf
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
convex_iff_pairwise_pos
LT.lt.le
add_le_add
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
smul_le_smul_of_nonneg_left
le_of_lt
Convex.combo_self
dual 📖mathematicalStrictConvexOnStrictConcaveOn
OrderDual
OrderDual.instAddCommMonoid
OrderDual.instPartialOrder
OrderDual.instSMul
DFunLike.coe
Equiv
EquivLike.toFunLike
Equiv.instEquivLike
OrderDual.toDual
eq_of_isMinOn 📖StrictConvexOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
IsMinOn
PartialOrder.toPreorder
Set
Set.instMembership
Nat.instAtLeastTwoHAddOfNat
PosMulReflectLE.toPosMulReflectLT
PosMulStrictMono.toPosMulReflectLE
IsStrictOrderedRing.toPosMulStrictMono
IsStrictOrderedRing.toIsOrderedRing
Mathlib.Meta.NormNum.isNat_eq_true
Mathlib.Meta.NormNum.IsNNRat.to_isNat
Mathlib.Meta.NormNum.isNNRat_add
Mathlib.Meta.NormNum.isNNRat_inv_pos
IsStrictOrderedRing.toCharZero
Mathlib.Meta.NormNum.IsNat.to_isNNRat
Mathlib.Meta.NormNum.isNat_ofNat
Mathlib.Meta.NormNum.instAtLeastTwo
Nat.cast_one
lt_irrefl
instNontrivialOfCharZero
add_le_add
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
smul_le_smul_of_nonneg_left
le_of_lt
inv_pos_of_pos
Mathlib.Meta.Positivity.pos_of_isNat
add_smul
Mathlib.Meta.NormNum.IsNat.to_eq
one_smul
lt_on_openSegment 📖mathematicalStrictConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
openSegment
Preorder.toLT
PartialOrder.toPreorder
SemilatticeSup.toMax
Lattice.toSemilatticeSup
lt_on_open_segment'
lt_on_open_segment' 📖mathematicalStrictConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set
Set.instMembership
Preorder.toLT
PartialOrder.toPreorder
MulZeroClass.toZero
NonUnitalNonAssocSemiring.toMulZeroClass
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
SemilatticeSup.toMax
Lattice.toSemilatticeSup
add_le_add
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
smul_le_smul_of_nonneg_left
PosSMulStrictMono.toPosSMulMono
le_max_left
le_of_lt
le_max_right
Convex.combo_self
neg 📖mathematicalStrictConvexOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
StrictConcaveOn
Pi.instNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
neg_strictConcaveOn_iff
sub 📖mathematicalStrictConvexOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
StrictConcaveOn
Pi.instSub
SubNegMonoid.toSub
add
IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
StrictConcaveOn.neg
sub_eq_add_neg
sub_concaveOn 📖mathematicalStrictConvexOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
ConcaveOn
Pi.instSub
SubNegMonoid.toSub
add_convexOn
IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
ConcaveOn.neg
sub_eq_add_neg
subset 📖StrictConvexOn
Set
Set.instHasSubset
Convex
sup 📖mathematicalStrictConvexOn
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instMaxForall_mathlib
SemilatticeSup.toMax
Lattice.toSemilatticeSup
max_lt
add_le_add
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
smul_le_smul_of_nonneg_left
PosSMulStrictMono.toPosSMulMono
le_sup_left
le_of_lt
le_sup_right
translate_left 📖mathematicalStrictConvexOn
AddCancelCommMonoid.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
add_comm
translate_right
translate_right 📖mathematicalStrictConvexOn
AddCancelCommMonoid.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Set.preimage
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
Convex.translate_preimage_right
smul_add
add_add_add_comm
Convex.combo_self
add_right_injective
AddLeftCancelSemigroup.toIsLeftCancelAdd

(root)

Definitions

NameCategoryTheorems
ConcaveOn 📖MathDef
32 mathmath: concaveOn_id, ConvexOn.smul'', AntitoneOn.concaveOn_of_deriv, concaveOn_iff_slope_anti_adjacent, concaveOn_of_slope_anti_adjacent, strongConcaveOn_zero, neg_convexOn_iff, Real.concaveOn_rpow, OrderIso.concaveOn_symm, concaveOn_of_deriv2_nonpos', concaveOn_iff_div, ConvexOn.neg, concaveOn_of_hasDerivWithinAt2_nonpos, neg_concaveOn_iff, strongConcaveOn_iff_convex, concaveOn_univ_of_deriv2_nonpos, LinearOrder.concaveOn_of_lt, Real.concaveOn_negMulLog, ConvexOn.dual, concaveOn_of_convex_hypograph, UniformConcaveOn.concaveOn, uniformConcaveOn_zero, LinearMap.concaveOn, concaveOn_of_deriv2_nonpos, concaveOn_iff_pairwise_pos, concaveOn_iff_forall_pos, ConvexOn.mul', Antitone.concaveOn_univ_of_deriv, StrictConcaveOn.concaveOn, concaveOn_iff_convex_hypograph, concaveOn_const, NNReal.concaveOn_rpow
ConvexOn 📖MathDef
47 mathmath: convexOn_of_hasDerivWithinAt2_nonneg, convexOn_id, convexOn_univ_dist, ConcaveOn.smul'', MonotoneOn.convexOn_of_deriv, convexOn_of_deriv2_nonneg', convexOn_rpow_left, convexOn_dist, convexOn_iff_forall_pos, Seminorm.convexOn, convexOn_univ_norm, neg_convexOn_iff, LinearOrder.convexOn_of_lt, ConcaveOn.mul', Real.convexOn_log_Gamma, UniformConvexOn.convexOn, neg_concaveOn_iff, convexOn_of_convex_epigraph, Real.doublingGamma_log_convex_Ioi, convexOn_of_deriv2_nonneg, convexOn_descPochhammer_eval, Real.convexOn_Gamma, LinearMap.convexOn, InformationTheory.convexOn_klFun, Monotone.convexOn_univ_of_deriv, convexOn_of_slope_mono_adjacent, convexOn_pow, ConcaveOn.neg, convexOn_exp, InformationTheory.convexOn_Ioi_klFun, convexOn_univ_of_deriv2_nonneg, StrictConvexOn.convexOn, OrderIso.convexOn_symm, strongConvexOn_iff_convex, strongConvexOn_zero, convexOn_iff_div, Even.convexOn_pow, convexOn_const, convexOn_zpow, Real.convexOn_mul_log, convexOn_iff_convex_epigraph, ConcaveOn.dual, convexOn_rpow, uniformConvexOn_zero, convexOn_iff_pairwise_pos, convexOn_norm, convexOn_iff_slope_mono_adjacent
StrictConcaveOn 📖MathDef
29 mathmath: LinearOrder.strictConcaveOn_of_lt, Real.strictConcaveOn_rpow, StrictConvexOn.neg, neg_strictConvexOn_iff, strictConcaveOn_log_Iio, strictConcaveOn_univ_of_deriv2_neg, NNReal.strictConcaveOn_sqrt, strictConcaveOn_sqrt_mul_log_Ioi, strictConcaveOn_iff_slope_strict_anti_adjacent, StrongConcaveOn.strictConcaveOn, StrictAntiOn.strictConcaveOn_of_deriv, UniformConcaveOn.strictConcaveOn, Real.strictConcaveOn_sqrt, StrictAnti.strictConcaveOn_univ_of_deriv, strictConcaveOn_sin_Icc, strictConcaveOn_iff_div, strictConcaveOn_of_deriv2_neg', StrictConvexOn.dual, Real.strictConcave_binEntropy, strictConcaveOn_log_Ioi, strictConcaveOn_of_deriv2_neg, strictConcaveOn_of_slope_strict_anti_adjacent, OrderIso.strictConcaveOn_symm, neg_strictConcaveOn_iff, strictConcaveOn_cos_Icc, NNReal.strictConcaveOn_rpow, Real.strictConcaveOn_negMulLog, ConcaveOn.sub_strictConvexOn, Real.strictConcaveOn_qaryEntropy
StrictConvexOn 📖MathDef
24 mathmath: strictConvexOn_iff_slope_strict_mono_adjacent, neg_strictConvexOn_iff, strictConvexOn_pow, UniformConvexOn.strictConvexOn, OrderIso.strictConvexOn_symm, strictConvexOn_exp, LinearOrder.strictConvexOn_of_lt, Even.strictConvexOn_pow, StrictMonoOn.strictConvexOn_of_deriv, Real.strictConvexOn_mul_log, StrictMono.strictConvexOn_univ_of_deriv, strictConvexOn_rpow, strictConvexOn_of_slope_strict_mono_adjacent, strictConvexOn_of_deriv2_pos', ConvexOn.sub_strictConcaveOn, InformationTheory.strictConvexOn_klFun, StrictConcaveOn.neg, strictConvexOn_univ_of_deriv2_pos, StrongConvexOn.strictConvexOn, strictConvexOn_zpow, StrictConcaveOn.dual, strictConvexOn_iff_div, neg_strictConcaveOn_iff, strictConvexOn_of_deriv2_pos

Theorems

NameKindAssumesProvesValidatesDepends On
concaveOn_const 📖mathematicalConvexConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
convexOn_const
concaveOn_id 📖mathematicalConvexConcaveOnle_refl
concaveOn_iff_convex_hypograph 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
Prod.instAddCommMonoid
Prod.instSMul
setOf
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
convexOn_iff_convex_epigraph
OrderDual.isOrderedAddMonoid
OrderDual.instPosSMulMono
concaveOn_iff_div 📖mathematicalConcaveOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
Convex
Preorder.toLE
PartialOrder.toPreorder
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
DivInvMonoid.toDiv
DivisionRing.toDivInvMonoid
Field.toDivisionRing
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
NonUnitalCommRing.toNonUnitalNonAssocCommRing
CommRing.toNonUnitalCommRing
Field.toCommRing
convexOn_iff_div
concaveOn_iff_forall_pos 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
Preorder.toLE
PartialOrder.toPreorder
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
convexOn_iff_forall_pos
concaveOn_iff_pairwise_pos 📖mathematicalConcaveOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
Set.Pairwise
convexOn_iff_pairwise_pos
concaveOn_of_convex_hypograph 📖mathematicalConvex
Prod.instAddCommMonoid
Prod.instSMul
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
setOf
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
ConcaveOnconvexOn_of_convex_epigraph
convexOn_const 📖mathematicalConvexConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Eq.ge
Convex.combo_self
convexOn_id 📖mathematicalConvexConvexOnle_refl
convexOn_iff_convex_epigraph 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
Prod.instAddCommMonoid
Prod.instSMul
setOf
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
ConvexOn.convex_epigraph
convexOn_of_convex_epigraph
convexOn_iff_div 📖mathematicalConvexOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
Convex
Preorder.toLE
PartialOrder.toPreorder
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
DivInvMonoid.toDiv
DivisionRing.toDivInvMonoid
Field.toDivisionRing
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
NonUnitalCommRing.toNonUnitalNonAssocCommRing
CommRing.toNonUnitalCommRing
Field.toCommRing
div_nonneg
PosMulReflectLE.toPosMulReflectLT
PosMulStrictMono.toPosMulReflectLE
IsStrictOrderedRing.toPosMulStrictMono
LT.lt.le
add_div
div_self
LT.lt.ne'
IsStrictOrderedRing.toZeroLEOneClass
NeZero.charZero_one
IsStrictOrderedRing.toCharZero
div_one
convexOn_iff_forall_pos 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
Preorder.toLE
PartialOrder.toPreorder
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
LT.lt.le
LE.le.eq_or_lt
zero_smul
zero_add
one_smul
add_zero
convexOn_iff_pairwise_pos 📖mathematicalConvexOn
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Convex
Set.Pairwise
convexOn_iff_forall_pos
eq_or_ne
Convex.combo_self
le_refl
convexOn_of_convex_epigraph 📖mathematicalConvex
Prod.instAddCommMonoid
Prod.instSMul
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
AddCommMonoid.toAddMonoid
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
setOf
Set
Set.instMembership
Preorder.toLE
PartialOrder.toPreorder
ConvexOnle_rfl
neg_concaveOn_iff 📖mathematicalConcaveOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
ConvexOn
neg_convexOn_iff
neg_neg
neg_convexOn_iff 📖mathematicalConvexOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
ConcaveOn
smul_neg
covariant_swap_add_of_covariant_add
IsOrderedAddMonoid.toAddLeftMono
add_comm
neg_le_neg_iff
neg_add
neg_neg
neg_strictConcaveOn_iff 📖mathematicalStrictConcaveOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
StrictConvexOn
neg_strictConvexOn_iff
neg_neg
neg_strictConvexOn_iff 📖mathematicalStrictConvexOn
AddCommGroup.toAddCommMonoid
SMulZeroClass.toSMul
AddZero.toZero
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
DistribSMul.toSMulZeroClass
DistribMulAction.toDistribSMul
MonoidWithZero.toMonoid
Semiring.toMonoidWithZero
Module.toDistribMulAction
Pi.instNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
StrictConcaveOn
smul_neg
IsRightCancelAdd.addRightStrictMono_of_addRightMono
AddRightCancelSemigroup.toIsRightCancelAdd
covariant_swap_add_of_covariant_add
IsOrderedAddMonoid.toAddLeftMono
add_comm
neg_lt_neg_iff
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
AddLeftCancelSemigroup.toIsLeftCancelAdd
neg_add
neg_neg
strictConcaveOn_iff_div 📖mathematicalStrictConcaveOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
Convex
Preorder.toLT
PartialOrder.toPreorder
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
DivInvMonoid.toDiv
DivisionRing.toDivInvMonoid
Field.toDivisionRing
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
NonUnitalCommRing.toNonUnitalNonAssocCommRing
CommRing.toNonUnitalCommRing
Field.toCommRing
strictConvexOn_iff_div
strictConvexOn_iff_div 📖mathematicalStrictConvexOn
DivisionSemiring.toSemiring
Semifield.toDivisionSemiring
Field.toSemifield
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
Convex
Preorder.toLT
PartialOrder.toPreorder
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
DivInvMonoid.toDiv
DivisionRing.toDivInvMonoid
Field.toDivisionRing
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
NonUnitalCommRing.toNonUnitalNonAssocCommRing
CommRing.toNonUnitalCommRing
Field.toCommRing
add_pos
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
AddLeftCancelSemigroup.toIsLeftCancelAdd
IsOrderedAddMonoid.toAddLeftMono
IsOrderedRing.toIsOrderedAddMonoid
IsStrictOrderedRing.toIsOrderedRing
div_pos
PosMulReflectLE.toPosMulReflectLT
PosMulStrictMono.toPosMulReflectLE
IsStrictOrderedRing.toPosMulStrictMono
add_div
div_self
LT.lt.ne'
div_one

---

← Back to Index