le_iff_forall_lt_one_mul_le — Mathlib

English

In a densely ordered group with a linear order and left-mono, we have a ≤ b if and only if for all ε < 1, a·ε ≤ b.

Русский

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

LaTeX

$$$a \le b \iff \forall \varepsilon,\ \varepsilon < 1 \rightarrow a \varepsilon \le b$$$

Lean4

@[to_additive]
theorem le_iff_forall_lt_one_mul_le : a ≤ b ↔ ∀ ε < 1, a * ε ≤ b :=
  le_iff_forall_one_lt_le_mul (α := αᵒᵈ)

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