English
Let a, b, c ∈ EReal with certain non-top conditions; if for all a' > a and all b' > b we have c ≤ a' · b', then c ≤ a · b.
Русский
Пусть a, b, c ∈ EReal и выполняются некоторые условия, предотвращающие верхнюю грань; если для всех a' > a и для всех b' > b выполняется c ≤ a' · b', то c ≤ a · b.
LaTeX
$$$(0 < a) \lor (b \neq \top) \rightarrow (a \neq \top) \lor (0 < b) \rightarrow (∀ a' > a, ∀ b' > b, c ≤ a' \cdot b') \Rightarrow c ≤ a \cdot b$$$
Lean4
theorem le_mul_of_forall_lt (h₁ : 0 < a ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ 0 < b) (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') :
c ≤ a * b := by
refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_
obtain ⟨a', aa', hd⟩ := exists_mul_left_lt (h₁.imp_left ne_of_gt) h₂ hd
replace h₁ : 0 < a' ∨ b ≠ ⊤ := h₁.imp_left fun a0 ↦ a0.trans (mem_Ioo.1 aa').1
replace h₂ : a' ≠ ⊤ ∨ b ≠ 0 := Or.inl (mem_Ioo.1 aa').2.ne
obtain ⟨b', bb', hd⟩ := exists_mul_right_lt h₁ h₂ hd
exact (h a' (mem_Ioo.1 aa').1 b' (mem_Ioo.1 bb').1).trans hd.le
