div_le_one_of_le₀ — Mathlib

English

Let the underlying set be an ordered group with zero. If a ≤ b and 0 ≤ b, then a/b ≤ 1.

Русский

Пусть имеется упорядоченная группа с нулём. Если a ≤ b и 0 ≤ b, то a/b ≤ 1.

LaTeX

$$$a,b \in G \land 0 \le b \land a \le b \Rightarrow \frac{a}{b} \le 1$$$

Lean4

@[bound]
theorem div_le_one_of_le₀ [ZeroLEOneClass G₀] (h : a ≤ b) (hb : 0 ≤ b) : a / b ≤ 1 :=
  div_le_of_le_mul₀ hb zero_le_one <| by rwa [one_mul]

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