Commit 2023-03-25 07:07 5a447a0c

View on Github →

feat: port LinearAlgebra.AffineSpace.Ordered (#3094)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/AffineSpace/Ordered.lean

added theorem left_le_lineMap_iff_le

added theorem left_le_midpoint

added theorem left_lt_lineMap_iff_lt

added theorem lineMap_le_left_iff_le

added theorem lineMap_le_lineMap_iff_of_lt

added theorem lineMap_le_map_iff_slope_le_slope

added theorem lineMap_le_map_iff_slope_le_slope_left

added theorem lineMap_le_map_iff_slope_le_slope_right

added theorem lineMap_le_right_iff_le

added theorem lineMap_lt_left_iff_lt

added theorem lineMap_lt_lineMap_iff_of_lt

added theorem lineMap_lt_map_iff_slope_lt_slope

added theorem lineMap_lt_map_iff_slope_lt_slope_left

added theorem lineMap_lt_map_iff_slope_lt_slope_right

added theorem lineMap_lt_right_iff_lt

added theorem lineMap_mono_endpoints

added theorem lineMap_mono_left

added theorem lineMap_mono_right

added theorem lineMap_strict_mono_endpoints

added theorem lineMap_strict_mono_left

added theorem lineMap_strict_mono_right

added theorem map_le_lineMap_iff_slope_le_slope

added theorem map_le_lineMap_iff_slope_le_slope_left

added theorem map_le_lineMap_iff_slope_le_slope_right

added theorem map_lt_lineMap_iff_slope_lt_slope

added theorem map_lt_lineMap_iff_slope_lt_slope_left

added theorem map_lt_lineMap_iff_slope_lt_slope_right

added theorem midpoint_le_left

added theorem midpoint_le_midpoint

added theorem midpoint_le_right

added theorem right_le_lineMap_iff_le

added theorem right_le_midpoint

added theorem right_lt_lineMap_iff_lt