div_le_iff_le_mul — Mathlib

English

Let a, b, c ∈ EReal with similar non-top conditions; if for all a' > a, ∀ b' > b, 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 div_le_iff_le_mul (h : 0 < b) (h' : b ≠ ⊤) : a / b ≤ c ↔ a ≤ b * c :=
  by
  nth_rw 1 [← @mul_div_cancel c b (ne_bot_of_gt h) h' (ne_of_gt h)]
  rw [mul_div b c b, mul_comm b]
  exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Похожие утверждения