English
For Exists i, p i, then biSup_add' holds: (iSup i, iSup x, f i) + a = iSup i, iSup x, a + f i.
Русский
Для Существует i, p i, выполняется би-супремум добавления: (iSup i, iSup x, f i) + a = iSup i, iSup x, a + f i).
LaTeX
$$$ \exists i, p(i) \rightarrow \left( \iSup_i \iSup_x^{p(i)} f(i) + a = \iSup_i \iSup_x^{p(i)} (a + f(i)) \right) $$$
Lean4
theorem sub_iSup [Nonempty ι] (ha : a ≠ ⊤) : a - ⨆ i, f i = ⨅ i, a - f i :=
by
obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)
· rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, (iInf_eq_bot _).2, bot_eq_zero]
exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩
simp_rw [not_exists, not_lt] at h
refine
le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
ENat.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <| iSup_le fun i ↦ ?_
rw [← ENat.sub_sub_cancel ha (h _)]
exact tsub_le_tsub_left (iInf_le (a - f ·) i) _
