English
Let a, b, c ∈ EReal with certain non-top conditions; if for all a' > a and all b' > b we have a' · b' ≤ c, then c ≤ a · b.
Русский
Пусть a, b, c ∈ EReal и выполняются некоторые условия, ограничивающие верхнюю границу; если для всех a' > a и b' > b выполняется a'·b' ≤ c, то c ≤ a·b.
LaTeX
$$$(0 < a \lor b \neq \top) \land (a \neq \top \lor 0 < b) \land (∀ a' > a, ∀ b' > b, c ≤ a' \cdot b') \Rightarrow c ≤ a \cdot b$$$
Lean4
theorem le_div_iff_mul_le (h : b > 0) (h' : b ≠ ⊤) : a ≤ c / b ↔ a * b ≤ c :=
by
nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' (ne_of_gt h)]
rw [mul_div b a b, mul_comm a b]
exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')
