mathlib3

cb48031c - feat(analysis/convex/between): `wbtw_line_map_iff`, `sbtw_line_map_iff` (#17685)

feat(analysis/convex/between): `wbtw_line_map_iff`, `sbtw_line_map_iff` (#17685) Add lemmas giving `iff` conditions for `wbtw R x (line_map x y r) y` and `sbtw R x (line_map x y r) y` (assuming `[no_zero_smul_divisors R V]`).