Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-14 04:04 33406172

View on Github →

feat(algebra/bounds): smul of upper/lower bounds (#9078) This relates lower_bounds (a • s)/upper_bounds (a • s) and a • lower_bounds s/a • upper_bounds s.

Estimated changes

Modified src/algebra/module/ordered.lean

added theorem bdd_above.smul_of_nonneg

added theorem bdd_above.smul_of_nonpos

added theorem bdd_above_smul_iff_of_neg

added theorem bdd_above_smul_iff_of_pos

added theorem bdd_below.smul_of_nonneg

added theorem bdd_below.smul_of_nonpos

added theorem bdd_below_smul_iff_of_neg

added theorem bdd_below_smul_iff_of_pos

added theorem lower_bounds_smul_of_neg

added theorem lower_bounds_smul_of_pos

added theorem smul_lower_bounds_subset_lower_bounds_smul

added theorem smul_lower_bounds_subset_upper_bounds_smul

added theorem smul_upper_bounds_subset_lower_bounds_smul

added theorem smul_upper_bounds_subset_upper_bounds_smul

added theorem upper_bounds_smul_of_neg

added theorem upper_bounds_smul_of_pos