English
Let hf and hg provide non-∞ elements; if ha provides a bound a ≤ f_i · g_j for all i, j, then a ≤ (⨅ i, f_i) · (⨅ j, g_j).
Русский
Пусть hf и hg дают ненулевые пределы; если ha задаёт верхнюю грань a ≤ f_i · g_j для всех i, j, то a ≤ (⨅ i, f_i) · (⨅ j, g_j).
LaTeX
$$$\\exists_i f_i \\neq \\infty, \\exists_j g_j \\neq \\infty \\Rightarrow (\\inf_i u_i) (\\inf_j v_j) \\le \\inf_{i,j} u_i v_j$$$
Lean4
theorem le_iInf_mul_iInf {g : κ → ℝ≥0∞} (hf : ∃ i, f i ≠ ∞) (hg : ∃ j, g j ≠ ∞) (ha : ∀ i j, a ≤ f i * g j) :
a ≤ (⨅ i, f i) * ⨅ j, g j := by
rw [← iInf_ne_top_subtype]
have := nonempty_subtype.2 hf
have := hg.nonempty
replace hg : ⨅ j, g j ≠ ∞ := by simpa using hg
rw [iInf_mul fun h ↦ (hg h).elim, le_iInf_iff]
rintro ⟨i, hi⟩
simpa [mul_iInf fun h ↦ (hi h).elim] using ha i
