Sum of Inf is Inf of sum

Stream: Is there code for X?

[Pierre-Alexandre Bazin]

example {X Y : Type} (a : X → ℝ) (b : Y → ℝ) : ((⨅ x, a x) + (⨅ y, b y) = ⨅ (x : X) (y : Y), a x + b y) := begin library_search end

do we have a lemma stating this ?

[Pierre-Alexandre Bazin]

I asked the same question on the discord, and it seems it's false if X or Y are empty. So the lemma would have to include X or Y non empty in hypotheses, and maybe it's also wrong if the inf is -infinity (i don't know how it behaves in Lean in this case)

[Chris B]

Looks like https://leanprover-community.github.io/mathlib_docs/data/pi.html#pi.add_def

[Chris B]

The has_add (f i) assumption would function as the nonempty assumption I guess.

[Chris B]

Well, I guess not now that I think about it.

[Anne Baanen]

This is about the infimum operator ⨅, not the dependent function Π :)

[Chris B]

I've been had.

[Vincent Beffara]

Inf of a set that is empty or not bounded below gives (if I understand the code) 0 so the equality is also wrong if one of the infs on the left is -infinity and the other is not.

[Stuart Presnell]

If you add the required hypotheses to the lemma does library_search find anything?

[Pierre-Alexandre Bazin]

still nothing found for
example {X Y : Type} (a : X → ℝ≥0) (b : Y → ℝ≥0) (x : X) (y : Y) : ((⨅ x, a x) + (⨅ y, b y) = ⨅ (x : X) (y : Y), a x + b y) := begin library_search end

[Eric Wieser]

That's false when Y is empty and X is not, isn't it? In that case, it's infi a + 0 = 0, which is not true for all a

[Pierre-Alexandre Bazin]

I added (x : X) and (y : Y) in hypotheses so that X and Y are non empty

[Floris van Doorn]

I don't think we have it, but docs#ennreal.infi_add_infi is related. Especially the proof is interesting, because your statement is proven as part of it (for ennreal).

[Floris van Doorn]

You can probably mimic that proof to get the version for real using the dual versions of docs#csupr_add and docs#add_csupr (which seem to be missing).
You are right that you have to think about boundedness: the infimum of a set of reals that is not bounded below is defined to be 0.