Zulip Chat Archive

Stream: Is there code for X?

Topic: line_map


view this post on Zulip Scott Morrison (Mar 18 2021 at 22:42):

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.

view this post on Zulip Scott Morrison (Mar 18 2021 at 22:47):

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?

view this post on Zulip Yury G. Kudryashov (Mar 19 2021 at 03:36):

Indeed, these lemmas are missing.

view this post on Zulip Scott Morrison (Mar 19 2021 at 03:36):

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. :-)


Last updated: May 17 2021 at 16:26 UTC