English
If a ≠ ∞, then a − ⨆ i f_i = ⨅ i (a − f_i).
Русский
Если a ≠ ∞, то a − ⨆_i f_i = ⨅_i (a − f_i).
LaTeX
$$$\\text{If } a \\neq \\infty:\\; a - \\sup_i f_i = \\inf_i (a - f_i)$$$
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 ..) _) <|
ENNReal.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 [← sub_sub_cancel ha (h _)]
exact tsub_le_tsub_left (iInf_le (a - f ·) i) _
