le_of_forall_one_lt_div_le — Mathlib

English

In a densely ordered group with a linear order and left-m monotone multiplication, if a/ε ≤ b for every ε > 1, then a ≤ b.

Русский

В плотном упорядоченном групповом контексте с линейным порядком и монотонностью слева по умножению, если для любого ε > 1 выполняется a/ε ≤ b, то a ≤ b.

LaTeX

$$$\big( \forall \varepsilon,\ 1<\varepsilon \rightarrow a/\varepsilon \le b \big) \rightarrow a \le b$$$

Lean4

@[to_additive]
theorem le_of_forall_one_lt_div_le (h : ∀ ε : α, 1 < ε → a / ε ≤ b) : a ≤ b :=
  le_of_forall_lt_one_mul_le fun ε ε1 => by simpa only [div_eq_mul_inv, inv_inv] using h ε⁻¹ (Left.one_lt_inv_iff.2 ε1)

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