mul_le_of_forall_lt — Mathlib

English

If for all a' < a and b' < b we have a'·b' ≤ c, then a·b ≤ c.

Русский

Если для всех a'<a и b'<b выполняется a'·b' ≤ c, то a·b ≤ c.

LaTeX

$$$\big( \forall a'

Lean4

@[to_additive]
theorem mul_le_of_forall_lt [CommGroup α] [LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b c : α}
    (h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c) : a * b ≤ c :=
  by
  refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_
  obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd
  obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd
  exact hd.le.trans (h a' ha' b' hb')

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