line_map

Stream: Is there code for X?

[Scott Morrison]

Do we have a lemma saying a ≤ b -> 0 ≤ r -> a ≤ line_map a b r? I'm finding left_le_line_map_iff_le which is an iff version that assumes 0 < r.

[Scott Morrison]

Perhaps

lemma line_map_le_line_map_of_le_of_le (h : r ≤ r') (w : a ≤ b) :
  line_map a b r ≤ line_map a b r' :=
sorry

lemma left_le_line_map_of_nonneg_of_le (h : 0 ≤ r) (w : a ≤ b) :
  a ≤ line_map a b r :=
sorry

lemma line_map_le_right_of_le_one_of_le (h : r ≤ 1) (w : a ≤ b) :
  line_map a b r ≤ b :=
sorry

are missing in linear_algebra.affine_space.ordered?

[Yury G. Kudryashov]

Indeed, these lemmas are missing.

[Scott Morrison]

Okay. I have them installed in the right place in a branch full of sorries, and will get to them once they become the most exciting sorry remaining. :-)