smul_iInf_of_nonpos — Mathlib

English

Let a ≤ 0 and f: ι → ℝ. Then a times the infimum of {f(i)} equals the supremum over i of a times f(i): a · inf_i f(i) = sup_i a · f(i).

Русский

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

LaTeX

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

Lean4

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

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