Structures · Algebra
PosSMulStrictMono
Typeclass for strict monotonicity of scalar multiplication by positive elements on the left,
namely b₁ < b₂ → a • b₁ < a • b₂ if 0 < a.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsOrderedModule.
- Defined in
- Mathlib.Algebra.Order.Module.Defs
- Shape
- 2 explicit arguments · adds smul_lt_smul_of_pos_left
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances5
- Int
- Nat
- Rat
- NNReal
- NNRat
How is a type an instance?
Loading the hierarchy index…
Assumed by137
- smul_lt_smul_of_pos_left
- convex_Ioi
- Set.OrdConnected.strictConvex
- convex_Ico
- convex_Ioc
- smul_lt_smul_iff_of_pos_left
- convex_Iio
- ConvexCone.strictlyPositive
- smul_pos
- MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff
- smul_lt_smul_iff_of_neg_left
- MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff
- Finset.expect_lt_expect
- ConvexOn.le_left_of_right_le'
- ConvexOn.convex_lt
- ConvexOn.lt_left_of_right_lt'
- AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff
- smul_nonneg_iff_pos_imp_nonneg
- ConvexOn.le_left_of_right_le
- AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff
- strictMono_smul_left_of_pos
- smul_nonneg_iff
- AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff
- MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff
- openSegment_subset_Ioo
- ConvexOn.le_right_of_left_le
- convex_halfSpace_gt
- Finset.exists_le_of_expect_le_expect
- convex_halfSpace_lt
- ConvexOn.le_right_of_left_le'
- MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff
- ConvexOn.lt_right_of_left_lt'
- ConvexOn.lt_right_of_left_lt
- StrictConvexOn.lt_on_open_segment'
- ConvexOn.openSegment_subset_strict_epigraph
- ConvexOn.le_on_segment'
- smul_add_smul_lt_smul_add_smul
- convex_Ioo
- AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff
- ConvexOn.sup
- Antivary.sum_smul_comp_perm_eq_sum_smul_iff
- Antivary.sum_comp_perm_smul_eq_sum_smul_iff
- Antivary.sum_smul_lt_sum_smul_comp_perm_iff
- Antivary.sum_smul_lt_sum_comp_perm_smul_iff
- smul_lt_smul_of_neg_left
- ConvexOn.convex_strict_epigraph
- PosSMulStrictMono.smul_lt_smul_of_pos_left
- Monovary.sum_comp_perm_smul_lt_sum_smul_iff
- Monovary.sum_smul_comp_perm_lt_sum_smul_iff
- strictConvex_Ioc
Ancestors0
No ancestors.