smul_iSup_of_nonpos — Mathlib

English

Let a be a real number with a ≤ 0 and f an index-valued function f: ι → ℝ. Then a times the supremum of {f(i)} equals the infimum over i of a times f(i): a · sup_i f(i) = inf_i (a · f(i)).

Русский

Пусть a ∈ ℝ удовлетворяет a ≤ 0 и f: ι → ℝ. Тогда a· sup_i f(i) = inf_i a· f(i).

LaTeX

$$$ a \cdot \sup_{i} f(i) = \inf_{i} a \cdot f(i) $$$

Lean4

theorem smul_iSup_of_nonpos (ha : a ≤ 0) (f : ι → ℝ) : (a • ⨆ i, f i) = ⨅ i, a • f i :=
  (Real.sInf_smul_of_nonpos ha _).symm.trans <| congr_arg sInf <| (range_comp _ _).symm

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