English
If 0 ≤ a and 0 ≤ c and for all a' ≥ 0 < a and b' ≥ 0 < b we have a' b' ≤ c, then a b ≤ c.
Русский
Если 0 ≤ a и 0 ≤ c и для всех a' ≥ 0 < a и b' ≥ 0 < b верно a' b' ≤ c, то a b ≤ c.
LaTeX
$$$(ha : 0 \le a) (hc : 0 \le c) (h : ∀ a' \ge 0, a' < a \rightarrow ∀ b' \ge 0, b' < b \rightarrow a' * b' \le c) : a * b \le c$$
Lean4
theorem mul_le_of_forall_lt_of_nonneg {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c)
(h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c) : a * b ≤ c :=
by
refine le_of_forall_lt_imp_le_of_dense fun d d_ab ↦ ?_
rcases lt_or_ge d 0 with hd | hd
· exact hd.le.trans hc
obtain ⟨a', ha', d_ab⟩ := exists_lt_mul_left_of_nonneg ha hd d_ab
obtain ⟨b', hb', d_ab⟩ := exists_lt_mul_right_of_nonneg ha'.1 hd d_ab
exact d_ab.le.trans (h a' ha'.1 ha'.2 b' hb'.1 hb'.2)
