nnreal.le_div_iff

Stream: Is there code for X?

[Scott Morrison]

There are a few lemmas for linear_ordered_field that still work for ℝ≥0, such as the example below.

Do they already exist in mathlib? Is there a better way to prove things like this? Can they be generalized beyond ℝ≥0?

lemma nnreal.le_div_iff (a b c : ℝ≥0) (h : 0 < c) : a ≤ b / c ↔ a * c ≤ b :=
begin
  rcases a with ⟨a, a_pos⟩,
  rcases b with ⟨b, b_pos⟩,
  rcases c with ⟨c, c_pos⟩,
  change a ≤ b / c ↔ a * c ≤ b,
  change 0 < c at h,
  exact le_div_iff h,
end

[Scott Morrison]

Ah! Found it. One of the four is there, and the others can be proved the same way:

lemma nnreal.le_div_iff {a b c : ℝ≥0} (h : c ≠ 0) : a ≤ b / c ↔ a * c ≤ b :=
@le_div_iff ℝ _ a b c $ pos_iff_ne_zero.2 h

lemma nnreal.le_div_iff' {a b c : ℝ≥0} (h : c ≠ 0) : a ≤ b / c ↔ c * a ≤ b :=
@le_div_iff' ℝ _ a b c $ pos_iff_ne_zero.2 h

lemma nnreal.div_le_iff' {a b c : ℝ≥0} (h : b ≠ 0) : a / b ≤ c ↔ a ≤ b * c :=
@div_le_iff' ℝ _ a b c $ pos_iff_ne_zero.2 h

[Floris van Doorn]

@Damiano Testa To what extend can (are) these lemmas be generalized with the ordered refactor (#7645)?

[Damiano Testa]

@Floris van Doorn , the refactor has not reached rings yet: I am still generalizing algebraic structures with a single operation. Rings are next, of course, but I have not tested them yet. I think that this PR should go as is now and after the ordered refactor will have progressed, data will be modified to use it.

[Damiano Testa]

Btw, the current elaboration of #7645 successfully built on my machine: I am hopeful that CI will also build it successfully. In particular, the norm_num and linarith issues have been fixed!

[Sebastien Gouezel]

@Damiano Testa , the refactor is looking absolutely great. Thanks a lot for doing this!

[Damiano Testa]

Sébastien, I am glad that you like it! It is quite a bit of work, but it is also rewarding: I learned a lot about typeclasses!

[Kevin Buzzard]

Yes, this kind of work is great for learning a lot more about the system.

[Floris van Doorn]

Damiano Testa said:

Floris van Doorn , the refactor has not reached rings yet: I am still generalizing algebraic structures with a single operation. Rings are next, of course, but I have not tested them yet. I think that this PR should go as is now and after the ordered refactor will have progressed, data will be modified to use it.

Ah, that makes sense. These lemmas would currently fall into the ordered ring category. After the refactor they can probably (hopefully) be stated for ordered group_with_zero.