Zulip Chat Archive

Stream: Is there code for X?

Topic: monotone right inverse


view this post on Zulip Rémy Degenne (Jan 14 2021 at 09:28):

It feels like it should be somewhere, but I cannot find the following statement:

lemma function.right_inverse.monotone {α β} [linear_order α] [partial_order β]
  {g : α  β} {g_inv : β  α} (hg_right_inv : function.right_inverse g_inv g)
  (hg_mono : monotone g) :
  monotone g_inv :=
begin
  intros x y hxy,
  cases le_iff_lt_or_eq.mp hxy with h_lt h_eq,
  { rw [hg_right_inv x, hg_right_inv y] at h_lt,
    exact le_of_lt (monotone.reflect_lt hg_mono h_lt), },
  { rw h_eq, },
end

view this post on Zulip Heather Macbeth (Jan 14 2021 at 12:45):

Do you know about docs#order_embedding, docs#order_iso? I can't find the result you want in that file, but it seems like it might be its natural home ...

view this post on Zulip Rémy Degenne (Jan 14 2021 at 12:51):

yes I found order_iso about an hour ago and rewrote my proofs with it, which also made them simpler. Thanks!


Last updated: May 16 2021 at 05:21 UTC