ENNReal.le_iInf_add_iInf

Stream: Is there code for X?

[Eric Wieser]

We have docs#NNReal.le_iInf_add_iInf and docs#ENNReal.iInf_add_iInf; is the following true?

theorem ENNReal.le_iInf_add_iInf {ι ι' : Sort*} [Nonempty ι] [Nonempty ι'] {f : ι → ℝ≥0∞} {g : ι' → ℝ≥0∞}
    {a : ℝ≥0∞} (h : ∀ i j, a ≤ f i + g j) :
    a ≤ (⨅ i, f i) + ⨅ j, g j := by

is there a nicer argument than case splitting on whetherf and g are finite everywhere?

[Yury G. Kudryashov]

Try docs#ENNReal.add_iInf and docs#ENNReal.iInf_add

[Yury G. Kudryashov]

theorem ENNReal.le_iInf_add_iInf {ι ι' : Sort*} {f : ι → ℝ≥0∞} {g : ι' → ℝ≥0∞} {a : ℝ≥0∞}
    (h : ∀ i j, a ≤ f i + g j) :
    a ≤ (⨅ i, f i) + ⨅ j, g j := by
  simp only [add_iInf, iInf_add]
  exact le_iInf₂ fun _ _ ↦ h _ _

[Yaël Dillies]

Yes, the reason we don't have this lemma is that it's immediate from the two Yury quoted

[Eric Wieser]

I think the first two are worth combining for the same reason that we have add_add_add_comm

[Eric Wieser]

Yaël Dillies said:

Yes, the reason we don't have this lemma is that it's immediate from the two Yury quoted

Ah, and the NNReal one isn't because it's not a complete lattice?