Documentation Verification Report

Quasiconvex

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

Statistics

Metric	Count
Definitions `QuasiconcaveOn`, `QuasiconvexOn`, `QuasilinearOn`	3
Theorems `quasiconcaveOn`, `quasiconvexOn`, `quasilinearOn`, `quasiconcaveOn`, `quasiconvexOn`, `quasilinearOn`, `quasiconcaveOn`, `quasiconcaveOn_of_convex_ge`, `quasiconcaveOn_restrict`, `quasiconvexOn_of_convex_le`, `quasiconvexOn_restrict`, `quasiconvexOn`, `quasiconcaveOn`, `quasiconvexOn`, `quasilinearOn`, `quasiconcaveOn`, `quasiconvexOn`, `quasilinearOn`, `antitone_comp`, `convex`, `convex_gt`, `dual`, `inf`, `isPreconnected_preimage_subtype`, `monotone_comp`, `antitone_comp`, `convex`, `convex_lt`, `dual`, `isPreconnected_preimage_subtype`, `monotone_comp`, `sup`, `antitone_comp`, `dual`, `isPreconnected_preimage_subtype`, `monotoneOn_or_antitoneOn`, `monotone_comp`, `quasiconcaveOn_iff_min_le`, `quasiconvexOn_iff_le_max`, `quasilinearOn_iff_mem_uIcc`, `quasilinearOn_iff_monotoneOn_or_antitoneOn`	41
Total	44

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiconcaveOn` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`QuasiconcaveOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.univ`	—	`AntitoneOn.quasiconcaveOn` `antitoneOn` `convex_univ`
`quasiconvexOn` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`QuasiconvexOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.univ`	—	`AntitoneOn.quasiconvexOn` `antitoneOn` `convex_univ`
`quasilinearOn` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`QuasilinearOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.univ`	—	`quasiconvexOn` `quasiconcaveOn`

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiconcaveOn` 📖	mathematical	`AntitoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`QuasiconcaveOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`convex_ge`
`quasiconvexOn` 📖	mathematical	`AntitoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`QuasiconvexOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`convex_le`
`quasilinearOn` 📖	mathematical	`AntitoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`QuasilinearOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`quasiconvexOn` `quasiconcaveOn`

ConcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiconcaveOn` 📖	mathematical	`ConcaveOn` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`QuasiconcaveOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`convex_ge`

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiconcaveOn_of_convex_ge` 📖	mathematical	`Convex` `setOf`	`QuasiconcaveOn`	—	`quasiconvexOn_of_convex_le`
`quasiconcaveOn_restrict` 📖	mathematical	`QuasiconcaveOn` `Preorder.toLE` `Set` `Set.instHasSubset` `Convex`	`QuasiconcaveOn` `Preorder.toLE`	—	`Set.sep_eq_inter_sep` `inter`
`quasiconvexOn_of_convex_le` 📖	mathematical	`Convex` `setOf`	`QuasiconvexOn`	—	`inter`
`quasiconvexOn_restrict` 📖	mathematical	`QuasiconvexOn` `Preorder.toLE` `Set` `Set.instHasSubset` `Convex`	`QuasiconvexOn` `Preorder.toLE`	—	`Set.sep_eq_inter_sep` `inter`

ConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiconvexOn` 📖	mathematical	`ConvexOn` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`QuasiconvexOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`convex_le`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiconcaveOn` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`QuasiconcaveOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.univ`	—	`MonotoneOn.quasiconcaveOn` `monotoneOn` `convex_univ`
`quasiconvexOn` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`QuasiconvexOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.univ`	—	`MonotoneOn.quasiconvexOn` `monotoneOn` `convex_univ`
`quasilinearOn` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`QuasilinearOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.univ`	—	`quasiconvexOn` `quasiconcaveOn`

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiconcaveOn` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`QuasiconcaveOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`convex_ge`
`quasiconvexOn` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`QuasiconvexOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`convex_le`
`quasilinearOn` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`QuasilinearOn` `Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`quasiconvexOn` `quasiconcaveOn`

QuasiconcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_comp` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `QuasiconcaveOn` `Preorder.toLE`	`QuasiconvexOn` `Preorder.toLE`	—	`QuasiconvexOn.monotone_comp` `Antitone.dual`
`convex` 📖	mathematical	`QuasiconcaveOn`	`Convex`	—	`QuasiconvexOn.convex` `OrderDual.isDirected_le` `dual`
`convex_gt` 📖	mathematical	`QuasiconcaveOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Convex` `setOf` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`QuasiconvexOn.convex_lt` `dual`
`dual` 📖	mathematical	`QuasiconcaveOn`	`QuasiconvexOn` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`inf` 📖	mathematical	`QuasiconcaveOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`QuasiconcaveOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin`	—	`QuasiconvexOn.sup` `dual`
`isPreconnected_preimage_subtype` 📖	mathematical	`QuasiconcaveOn` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction`	`IsPreconnected` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.preimage` `Set.Ici`	—	`Topology.IsInducing.isPreconnected_image` `Topology.IsInducing.subtypeVal` `Set.image_preimage_eq_inter_range` `Subtype.range_coe` `Set.inter_comm` `Convex.isPreconnected` `IsTopologicalAddGroup.toContinuousAdd`
`monotone_comp` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `QuasiconcaveOn` `Preorder.toLE`	`QuasiconcaveOn` `Preorder.toLE`	—	`QuasiconvexOn.monotone_comp` `Monotone.dual`

QuasiconvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_comp` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `QuasiconvexOn` `Preorder.toLE`	`QuasiconcaveOn` `Preorder.toLE`	—	`monotone_comp`
`convex` 📖	mathematical	`QuasiconvexOn`	`Convex`	—	`exists_ge_ge`
`convex_lt` 📖	mathematical	`QuasiconvexOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Convex` `setOf` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_max_left` `le_max_right` `LE.le.trans_lt` `max_lt`
`dual` 📖	mathematical	`QuasiconvexOn`	`QuasiconcaveOn` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`isPreconnected_preimage_subtype` 📖	mathematical	`QuasiconvexOn` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction`	`IsPreconnected` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.preimage` `Set.Iic`	—	`QuasiconcaveOn.isPreconnected_preimage_subtype`
`monotone_comp` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `QuasiconvexOn` `Preorder.toLE`	`QuasiconvexOn` `Preorder.toLE`	—	`le_rfl` `le_trans`
`sup` 📖	mathematical	`QuasiconvexOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`QuasiconvexOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax`	—	`Set.sep_and` `Convex.inter`

QuasilinearOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_comp` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `QuasilinearOn` `Preorder.toLE`	`QuasilinearOn` `Preorder.toLE`	—	`QuasiconcaveOn.antitone_comp` `QuasiconvexOn.antitone_comp`
`dual` 📖	mathematical	`QuasilinearOn`	`QuasilinearOn` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`isPreconnected_preimage_subtype` 📖	mathematical	`QuasilinearOn` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction`	`IsPreconnected` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.preimage` `Set.Iic`	—	`QuasiconvexOn.isPreconnected_preimage_subtype`
`monotoneOn_or_antitoneOn` 📖	mathematical	`QuasilinearOn` `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` `Preorder.toLE` `PartialOrder.toPreorder` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AntitoneOn`	—	`Convex.segment_subset` `Set.sep_or` `instReflLe`
`monotone_comp` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `QuasilinearOn` `Preorder.toLE`	`QuasilinearOn` `Preorder.toLE`	—	`QuasiconvexOn.monotone_comp` `QuasiconcaveOn.monotone_comp`

(root)

Definitions

Name	Category	Theorems
`QuasiconcaveOn` 📖	MathDef	12 math math: `quasiconcaveOn_iff_min_le`, `Monotone.quasiconcaveOn`, `QuasiconcaveOn.monotone_comp`, `ConcaveOn.quasiconcaveOn`, `QuasiconcaveOn.inf`, `Convex.quasiconcaveOn_restrict`, `AntitoneOn.quasiconcaveOn`, `QuasiconvexOn.antitone_comp`, `QuasiconvexOn.dual`, `MonotoneOn.quasiconcaveOn`, `Convex.quasiconcaveOn_of_convex_ge`, `Antitone.quasiconcaveOn`
`QuasiconvexOn` 📖	MathDef	12 math math: `QuasiconcaveOn.antitone_comp`, `Convex.quasiconvexOn_of_convex_le`, `Antitone.quasiconvexOn`, `MonotoneOn.quasiconvexOn`, `QuasiconvexOn.sup`, `quasiconvexOn_iff_le_max`, `ConvexOn.quasiconvexOn`, `QuasiconvexOn.monotone_comp`, `AntitoneOn.quasiconvexOn`, `Monotone.quasiconvexOn`, `QuasiconcaveOn.dual`, `Convex.quasiconvexOn_restrict`
`QuasilinearOn` 📖	MathDef	9 math math: `QuasilinearOn.monotone_comp`, `Monotone.quasilinearOn`, `quasilinearOn_iff_monotoneOn_or_antitoneOn`, `QuasilinearOn.dual`, `MonotoneOn.quasilinearOn`, `AntitoneOn.quasilinearOn`, `Antitone.quasilinearOn`, `quasilinearOn_iff_mem_uIcc`, `QuasilinearOn.antitone_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiconcaveOn_iff_min_le` 📖	mathematical	—	`QuasiconcaveOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Convex` `SemilatticeInf.toMin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`quasiconvexOn_iff_le_max`
`quasiconvexOn_iff_le_max` 📖	mathematical	—	`QuasiconvexOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Convex` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`QuasiconvexOn.convex` `SemilatticeSup.instIsDirectedOrder` `le_max_left` `le_max_right` `LE.le.trans` `max_le`
`quasilinearOn_iff_mem_uIcc` 📖	mathematical	—	`QuasilinearOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Convex` `Set` `Set.instMembership` `Set.uIcc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`QuasilinearOn.eq_1` `quasiconvexOn_iff_le_max` `quasiconcaveOn_iff_min_le`
`quasilinearOn_iff_monotoneOn_or_antitoneOn` 📖	mathematical	`Convex` `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`	`QuasilinearOn` `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` `Preorder.toLE` `PartialOrder.toPreorder` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `MonotoneOn` `AntitoneOn`	—	`QuasilinearOn.monotoneOn_or_antitoneOn` `MonotoneOn.quasilinearOn` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `AntitoneOn.quasilinearOn`

---

← Back to Index