monotone right inverse

Stream: Is there code for X?

[Rémy Degenne]

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

[Heather Macbeth]

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

[Rémy Degenne]

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