le_mul_of_forall_lt₀ — Mathlib

English

If a ≥ 0, a' ≥ 0, a' < a, b' ≥ 0, b' < b and c ≤ a' b', then c ≤ a b.

Русский

Если a ≥ 0, a' ≥ 0, a' < a, b' ≥ 0, b' < b и c ≤ a' b', то c ≤ a b.

LaTeX

$$(ha : 0 ≤ a) (hc : 0 ≤ c) (h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c) : a * b ≤ c$$

Lean4

theorem le_mul_of_forall_lt₀ {a b c : α} (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', ha', hd⟩ := exists_mul_left_lt₀ hd
  obtain ⟨b', hb', hd⟩ := exists_mul_right_lt₀ hd
  exact (h a' ha' b' hb').trans hd.le

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