iInf_mul_of_nonpos

Mathlib.Data.Real.Pointwise

URI: https://scilib.ai/kg/mathlib#Real.iInf_mul_of_nonpos

English

For r ≤ 0 and f: ι → ℝ, the infimum commutes with multiplication: (inf_i f(i)) · r = inf_i (f(i) · r).

Русский

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

LaTeX

$$$ (\inf_{i} f(i)) \cdot r = \inf_{i} (f(i) \cdot r) $$$

Lean4

theorem iInf_mul_of_nonpos (ha : r ≤ 0) (f : ι → ℝ) : (⨅ i, f i) * r = ⨆ i, f i * r := by
  simp only [Real.mul_iInf_of_nonpos ha, mul_comm]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru