English
Let a, b, c ∈ EReal with non-top conditions; if for all a' ∈ (0, a) and all b' ∈ (0, b) we have a' · b' ≤ c, then a · b ≤ c.
Русский
Пусть a, b, c ∈ EReal с условиями, исключающими верхнюю границу; если для всех a' ∈ (0, a) и b' ∈ (0, b) выполняется a' · b' ≤ c, то a · b ≤ c.
LaTeX
$$$\text{If } a,b,c \in EReal \text{ and } (\forall a' \in (0,a), \forall b' \in (0,b), a' b' ≤ c) \text{ then } a b ≤ c$$$
Lean4
theorem mul_le_of_forall_lt_of_nonneg (ha : 0 ≤ a) (hc : 0 ≤ c) (h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c) :
a * b ≤ c := by
refine le_of_forall_lt_imp_le_of_dense fun d dab ↦ ?_
rcases lt_or_ge d 0 with d0 | d0
· exact d0.le.trans hc
obtain ⟨a', aa', dab⟩ := exists_lt_mul_left_of_nonneg ha d0 dab
obtain ⟨b', bb', dab⟩ := exists_lt_mul_right_of_nonneg aa'.1.le d0 dab
exact dab.le.trans (h a' aa' b' bb')
