supr₂_add

Stream: Is there code for X?

[Andrew Yang]

Do we have this result somewhere?

import data.nat.lattice

lemma with_top.supr₂_add (ι : Sort*) (p : ι → Sort*) (hs : Exists p)
  (f : ∀ (i : ι), p i → with_top ℕ) (x : with_top ℕ) :
  (⨆ (i : ι) (h : p i), f i h) + x = ⨆ (i : ι) (h : p i), f i h + x :=
sorry

Or the analogous result in ℕ with the additional condition of bdd_above (set.range f).

[Yaël Dillies]

docs#Sup_add, docs#cSup_add

[Andrew Yang]

Thanks! Sorry for the late reply, but it seems like it only works for groups, and the proof doesn't seem to generalize to monoids immediately.

[Yaël Dillies]

Yeah because it's wrong! But in ℕ you can use docs#cSup_image2_eq_cSup_cSup because + still has an adjoint, namely nat subtraction.

[Andrew Yang]

I think it would be faster to prove it straightforwardly? Thanks a lot anyways!

lemma with_top.supr_add {ι : Sort*} [nonempty ι]
  (f : ι → with_top ℕ) (x : with_top ℕ) :
  supr f + x = ⨆ i, f i + x :=
begin
  cases x, { simp_rw [with_top.none_eq_top, add_top, supr_const] },
  have : ↑x ≤ ⨆ i, f i + ↑x,
  { refine le_trans _ (le_supr _ $ classical.arbitrary _), exact le_add_left rfl.le },
  rw with_top.some_eq_coe,
  apply le_antisymm,
  { rw [← tsub_add_cancel_of_le this],
    refine add_le_add (supr_le $ λ i, _) rfl.le,
    apply (with_top.add_le_add_iff_right (with_top.coe_ne_top : (x : with_top ℕ) ≠ ⊤)).mp,
    rw [tsub_add_cancel_of_le this],
    exact le_supr _ i },
  { exact supr_le (λ i, add_le_add (le_supr f i) rfl.le) }
end

lemma with_top.supr₂_add {ι : Sort*} {p : ι → Sort*} (hs : Exists p)
  (f : ∀ (i : ι), p i → with_top ℕ) (x : with_top ℕ) :
  (⨆ (i : ι) (h : p i), f i h) + x = ⨆ (i : ι) (h : p i), f i h + x :=
begin
  haveI : nonempty { i // p i } := ⟨⟨_, hs.some_spec⟩⟩,
  rw [supr_subtype', supr_subtype', with_top.supr_add]
end