English
If s ⊆ t, and there are elements of t outside of s with strict positivity, then the product over s is less than the product over t.
Русский
Если s ⊆ t и существуют элементы вне s в t с положительным вкладом, то произведение по s меньше произведения по t.
LaTeX
$$$s \\subseteq t \\land \\exists i \\in t \\setminus s, 1 < f(i) \\Rightarrow \\prod_{i \\in s} f(i) < \\prod_{i \\in t} f(i)$$$
Lean4
@[to_additive sum_lt_sum_of_subset]
theorem prod_lt_prod_of_subset' (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i ∉ s) (hlt : 1 < f i)
(hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j) : ∏ j ∈ s, f j < ∏ j ∈ t, f j := by
classical
calc
∏ j ∈ s, f j < ∏ j ∈ insert i s, f j := by
rw [prod_insert hs]
exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt
_ ≤ ∏ j ∈ t, f j := by
apply prod_le_prod_of_subset_of_one_le'
· simp [Finset.insert_subset_iff, h, ht]
· intro x hx h'x
simp only [mem_insert, not_or] at h'x
exact hle x hx h'x.2
