Stream: Is there code for X?
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.
Scott Morrison (Mar 18 2021 at 22:47):
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
Yury G. Kudryashov (Mar 19 2021 at 03:36):
Indeed, these lemmas are missing.
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