English
For f, g : ι → ENNReal with appropriate non∞ conditions, (⨅ i, f_i) · (⨅ i, g_i) = ⨅ i, f_i · g_i.
Русский
Для f, g : ι → ENNReal при подходящих условиях нен∞: (⨅ i, f_i) · (⨅ i, g_i) = ⨅ i, f_i · g_i.
LaTeX
$$$\\left(\\inf_i f_i\\right) \\cdot \\left(\\inf_i g_i\\right) = \\inf_i \\bigl(f_i \\cdot g_i\\bigr)$$$
Lean4
theorem iInf_mul_iInf {f g : ι → ℝ≥0∞} (hf : ∃ i, f i ≠ ∞) (hg : ∃ j, g j ≠ ∞) (h : ∀ i j, ∃ k, f k * g k ≤ f i * g j) :
(⨅ i, f i) * ⨅ i, g i = ⨅ i, f i * g i :=
by
refine le_antisymm (le_iInf fun i ↦ mul_le_mul' (iInf_le ..) (iInf_le ..)) (le_iInf_mul_iInf hf hg fun i j ↦ ?_)
obtain ⟨k, hk⟩ := h i j
exact iInf_le_of_le k hk
