cmp_div_one' — Mathlib

English

Let α be a linear-ordered group. If for all ε with 1 < ε we have a < b ε, then a ≤ b.

Русский

Пусть α — линейно упорядоченная группа. Если для всякого ε с 1 < ε верно a < b ε, то a ≤ b.

LaTeX

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

Lean4

@[to_additive (attr := simp) cmp_sub_zero]
theorem cmp_div_one' [MulRightMono α] (a b : α) : cmp (a / b) 1 = cmp a b := by
  rw [← cmp_mul_right' _ _ b, one_mul, div_mul_cancel]

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