ennreal.to_nnreal_le_to_nnreal

Stream: Is there code for X?

[Kalle Kytölä]

I could not find the following by library_search or otherwise. Do we (not) have it?

import topology.instances.ennreal

open_locale ennreal

lemma ennreal.to_nnreal_le_to_nnreal {a b : ℝ≥0∞} (hab : a ≤ b) (hb : b ≠ ∞) :
  a.to_nnreal ≤ b.to_nnreal :=
begin
  apply (@ennreal.coe_le_coe a.to_nnreal b.to_nnreal).mp,
  simpa [hb, (lt_of_le_of_lt hab hb.lt_top).ne],
end

[Heather Macbeth]

Seems not -- maybe add using the same naming convention as docs#ennreal.to_real_le_to_real and docs#ennreal.to_real_mono?

[Yakov Pechersky]

It's a bit worse than mono because of the hb hypothesis. Golfed:

lemma ennreal.to_nnreal_le_to_nnreal {a b : ℝ≥0∞} (hab : a ≤ b) (hb : b ≠ ∞) :
  a.to_nnreal ≤ b.to_nnreal :=
by simpa [←ennreal.coe_le_coe, hb, (hab.trans_lt hb.lt_top).ne]

[Kalle Kytölä]

Thank you both!

PR #10556 (hopefully easy) with four such lemmas. I tried to follow exactly the same naming and hypothesis conventions as in the corresponding to_real versions, as Heather suggested, and I included Yakov's golf in two of the four.