Commit 2025-09-22 15:22 9c678d6d

View on Github →

feat(LinearAlgebra/AffineSpace/Ordered): add lineMap_le_lineMap_iff_of_lt' (#27257) I only need lineMap_le_lineMap_iff_of_lt'. The other lemmas are added for completeness.

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/Ordered.lean

added theorem left_le_lineMap_iff_nonneg

added theorem left_lt_lineMap_iff_pos

added theorem lineMap_le_left_iff_nonpos

added theorem lineMap_le_lineMap_iff_of_lt'

added theorem lineMap_le_right_iff_le_one

added theorem lineMap_lt_left_iff_neg

added theorem lineMap_lt_lineMap_iff_of_lt'

added theorem lineMap_lt_right_iff_lt_one

modified theorem midpoint_le_midpoint

added theorem right_le_lineMap_iff_one_le

added theorem right_lt_lineMap_iff_one_lt