iInf_mul_of_nonneg

Mathlib.Data.Real.Pointwise

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

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_nonneg (ha : 0 ≤ r) (f : ι → ℝ) : (⨅ i, f i) * r = ⨅ i, f i * r := by
  simp only [Real.mul_iInf_of_nonneg ha, mul_comm]

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

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

Разделы

Аффилиация

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