add_biSup' — Mathlib

English

If there exists i with a predicate p(i), then adding a to the nested supremums equals the nested supremums with a added inside: a + sup_i sup_{p(i)} f_i = sup_i sup_{p(i)} (a + f_i).

Русский

Если существует i с p(i), то a + ⨆_i ⨆_{p(i)} f_i = ⨆_i ⨆_{p(i)} (a + f_i).

LaTeX

$$$ a + \\bigl(\\sup_i \\sup_{p(i)} f_i\\bigr) = \\sup_i \\sup_{p(i)} (a + f_i) $$$

Lean4

theorem add_biSup' {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℝ≥0∞) : a + ⨆ i, ⨆ _ : p i, f i = ⨆ i, ⨆ _ : p i, a + f i :=
  by
  haveI : Nonempty { i // p i } := nonempty_subtype.2 h
  simp only [iSup_subtype', add_iSup]

Похожие утверждения