English
If f ≤ g and f i < g i for some i, with HasProd f a1 L and HasProd g a2 L, then a1 < a2.
Русский
Если f ≤ g и существует i с f i < g i, и HasProd f a1 L и HasProd g a2 L, то a1 < a2.
LaTeX
$$$\\forall f,g:\\, \\text{HasProd } f a_1 L \\to \\text{HasProd } g a_2 L \\to (f \\le g) \\to (f i < g i) \\to a_1 < a_2$$$
Lean4
@[to_additive]
theorem hasProd_lt [L.NeBot] [L.LeAtTop] (h : f ≤ g) (hi : f i < g i) (hf : HasProd f a₁ L) (hg : HasProd g a₂ L) :
a₁ < a₂ := by
classical
have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩
have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)
simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this
