iSup_sub — Mathlib

English

Let f_i: I → ℝ≥0∞ and a ∈ ℝ≥0∞. Then the truncated subtraction by a commutes with taking the supremum: sup_i f_i − a = sup_i (f_i − a).

Русский

Пусть f_i: I → ℝ≥0∞ и фиксировано a ∈ ℝ≥0∞. Тогда отсечение вычитания a от верхней грани коммутирует с взятием верхней грани: ⨆_i f_i − a = ⨆_i (f_i − a).

LaTeX

$$$\\biggl(\\sup_i f_i\\biggr) - a \\\\;=\\\\; \\sup_i (f_i - a)$$$

Lean4

theorem iSup_sub : (⨆ i, f i) - a = ⨆ i, f i - a :=
  le_antisymm (tsub_le_iff_right.2 <| iSup_le fun i => tsub_le_iff_right.1 <| le_iSup (f · - a) i)
    (iSup_le fun _ => tsub_le_tsub (le_iSup _ _) (le_refl a))

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