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	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.univ Set.piecewise Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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	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.univ Set.piecewise Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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	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.univ Set.piecewise Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.decidableMemIci LinearOrder.toDecidableLE	—	instReflLe 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	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.univ Set.piecewise Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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