Multiply `is_lub`

Stream: Is there code for X?

[Heather Macbeth]

Did I miss this somewhere in the library? If not, where should it go, and is there any meaningful generalization to some bigger class of ordered semirings than ℝ itself?

import data.real.basic

lemma real.is_lub_mul {s : set ℝ} {c : ℝ} (hc : 0 ≤ c) {A : ℝ} (hs : is_lub s A) :
  is_lub {x | ∃ a ∈ s, c * a = x} (c * A) :=
begin
  rcases lt_or_eq_of_le hc with hc | rfl, rotate,
  { convert is_lub_singleton using 1,
    ext x,
    have : s.nonempty ∧ 0 = x ↔ x = 0 := by rw [and_iff_right hs.nonempty, eq_comm],
    simpa using this },
  split,
  { rintros a ⟨a, ha, rfl⟩,
    exact mul_le_mul_of_nonneg_left (hs.1 ha) hc.le },
  { intros B hB,
    rw ← le_div_iff' hc,
    apply hs.2,
    intros a ha,
    rw le_div_iff' hc,
    exact hB ⟨a, ha, rfl⟩ }
end

[Heather Macbeth]

(It's true for ℝ≥0 but the proof looks different because it uses the nnreal rather than ordered_field versions of le_div_iff'.)

[Kevin Buzzard]

This is probably true for any continuous monotone function I guess, rather than just multiplication by c>=0

[Heather Macbeth]

Ah, so maybe I can use docs#order_iso.is_lub_image ...

[Heather Macbeth]

A little faster now, but the trivial case is still ugly:

lemma real.is_lub_mul {s : set ℝ} {c : ℝ} (hc : 0 ≤ c) {A : ℝ} (hs : is_lub s A) :
  is_lub {x | ∃ a ∈ s, c * a = x} (c * A) :=
begin
  rcases lt_or_eq_of_le hc with hc | rfl, rotate,
  { convert is_lub_singleton using 1,
    ext x,
    have : s.nonempty ∧ 0 = x ↔ x = 0 := by rw [and_iff_right hs.nonempty, eq_comm],
    simpa using this },
  rw ← (order_iso.mul_left₀ _ hc).is_lub_image' at hs,
  convert hs using 1,
  ext x,
  simp,
end

[Yaël Dillies]

file#data/real/pointwise is me proving similar stuff using the fact that $\R$ has default value 0.

[Heather Macbeth]

Nice! I just realized that in fact the version I wrote works over an arbitrary linear ordered field, which explains where I should put it. Maybe you could deduce your versions (which further requires the conditional completeness -- so, basically, ℝ) from it.

[Yaël Dillies]

Probably, yeah! I was about to say that your lemmas were the first part of my proof, but that's not really the case because I went through more real-specific lemmas.

[Yaël Dillies]

In my case, we need a refactor of docs#conditionally_complete_lattice to unbundle the default value, or create a class which states the default value.