English
Let α be a densely ordered group with linear order and left-mono. If for all a' > a and b' > b we have c ≤ a'·b', then c ≤ a·b.
Русский
Пусть α — плотный упорядоченный группы с линейным порядком и монотонностью слева. Если для всех a'>a и b'>b выполняется c ≤ a'·b', то c ≤ a·b.
LaTeX
$$$\big( \forall a'>a,\ \forall b'>b,\ c \le a' b' \big) \rightarrow c \le a b$$$
Lean4
@[to_additive]
theorem le_mul_of_forall_lt [CommGroup α] [LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {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
