English
If at index i in a finite set s we have g_i + h_i ≤ f_i and for all j ≠ i we have g_j ≤ f_j and h_j ≤ f_j, then (∏_{j∈s} g_j) + (∏_{j∈s} h_j) ≤ ∏_{j∈s} f_j.
Русский
Если на позиции i множества s выполняются условия g_i + h_i ≤ f_i и для всех j ≠ i выполняются g_j ≤ f_j и h_j ≤ f_j, тогда (∏ g_j) + (∏ h_j) ≤ ∏ f_j.
LaTeX
$$$\big(\prod_{j\in s} g(j)\big) + \big(\prod_{j\in s} h(j)\big) \le \prod_{j\in s} f(j)$$$
Lean4
/-- If `g, h ≤ f` and `g i + h i ≤ f i`, then the product of `f` over `s` is at least the
sum of the products of `g` and `h`. This is the version for `CanonicallyOrderedAdd`.
-/
theorem prod_add_prod_le' (hi : i ∈ s) (h2i : g i + h i ≤ f i) (hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j)
(hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j) : ((∏ i ∈ s, g i) + ∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i := by
classical
simp_rw [prod_eq_mul_prod_diff_singleton hi]
refine le_trans ?_ (mul_le_mul_right' h2i _)
rw [right_distrib]
gcongr with j hj j hj <;> simp_all
