English
If f ≤ g and some index j has f(j) < g(j) while other indices are bounded below by 1, then the HasProd values strictly compare: a1 < a2.
Русский
Если f ≤ g и существует индекс j с f(j) < g(j), а остальные индексы не менее 1, то HasProd f < HasProd g.
LaTeX
$$$\\forall f,g:\\, \\text{HasProd } f\\ a_1 L \\to \\text{HasProd } g\\ a_2 L \\to (f \\le g)\\to (\\exists i, f(i) < g(i)) \\to a_1 < a_2$$$
Lean4
@[to_additive]
theorem lt_hasProd [L.NeBot] [L.LeAtTop] [MulRightStrictMono α] (hf : HasProd f a L) (i : ι)
(hi : ∀ (j : ι), j ≠ i → 1 ≤ f j) (j : ι) (hij : j ≠ i) (hj : 1 < f j) : f i < a := by
classical
calc
f i < f j * f i := lt_mul_of_one_lt_left' (f i) hj
_ = ∏ k ∈ { j, i }, f k := by rw [Finset.prod_pair hij]
_ ≤ a := prod_le_hasProd _ (fun k hk ↦ hi k (hk ∘ mem_insert_of_mem ∘ mem_singleton.mpr)) hf
