le_iff_forall_one_lt_lt_mul — Mathlib

English

In a group with linear order, a ≤ b if and only if for all ε>1, a < b ε.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem le_iff_forall_one_lt_lt_mul : a ≤ b ↔ ∀ ε, 1 < ε → a < b * ε :=
  ⟨fun h _ => lt_mul_of_le_of_one_lt h, le_of_forall_one_lt_lt_mul⟩
    /-  I (DT) introduced this lemma to prove (the additive version `sub_le_sub_flip` of)
    `div_le_div_flip` below.  Now I wonder what is the point of either of these lemmas... -/

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