le_of_forall_lt_one_mul_le — Mathlib

English

If for all ε < 1 we have a·ε ≤ b, then a ≤ b (in a densely ordered group with left multiplication).

Русский

Если для всех ε < 1 выполняется a·ε ≤ b, то a ≤ b (в плотно упорядоченной группе с левой умножением).

LaTeX

$$$\forall \varepsilon < 1, \ a \cdot \varepsilon \le b \;\Rightarrow\; a \le b$$$

Lean4

@[to_additive]
theorem le_of_forall_lt_one_mul_le (h : ∀ ε < 1, a * ε ≤ b) : a ≤ b :=
  le_of_forall_one_lt_le_mul (α := αᵒᵈ) h

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