Piecewise

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

Statistics

Metric	Count
Definitions	0
Theorems concaveOn_univ_piecewise_Ici_of_antitoneOn_Ici_monotoneOn_Iic, concaveOn_univ_piecewise_Iic_of_monotoneOn_Iic_antitoneOn_Ici, convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic, convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
concaveOn_univ_piecewise_Ici_of_antitoneOn_Ici_monotoneOn_Iic 📖	mathematical	ConcaveOn AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iic AntitoneOn MonotoneOn	Set.univ Set.piecewise Set.decidableMemIci LinearOrder.toDecidableLE	—	neg_convexOn_iff Set.piecewise_neg convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic ConcaveOn.neg AntitoneOn.neg IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add MonotoneOn.neg
concaveOn_univ_piecewise_Iic_of_monotoneOn_Iic_antitoneOn_Ici 📖	mathematical	ConcaveOn AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ici MonotoneOn AntitoneOn	Set.univ Set.piecewise Set.decidableMemIic LinearOrder.toDecidableLE	—	neg_convexOn_iff Set.piecewise_neg convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici ConcaveOn.neg MonotoneOn.neg IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add AntitoneOn.neg
convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic 📖	mathematical	ConvexOn AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iic MonotoneOn AntitoneOn	Set.univ Set.piecewise Set.decidableMemIci LinearOrder.toDecidableLE	—	le_iff_lt_or_eq convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici
convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici 📖	mathematical	ConvexOn AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ici AntitoneOn MonotoneOn	Set.univ Set.piecewise Set.decidableMemIic LinearOrder.toDecidableLE	—	convex_univ le_or_gt LE.le.trans Convex.combo_le_max max_le Set.piecewise_eq_of_mem Set.piecewise_eq_of_notMem Set.notMem_Iic add_le_add_right IsOrderedAddMonoid.toAddLeftMono smul_le_smul_of_nonneg_left le_of_lt Set.self_mem_Iic Set.self_mem_Ici LT.lt.le add_le_add_left covariant_swap_add_of_covariant_add LT.lt.trans_le lt_min Convex.min_le_combo

---

← Back to Index