toAdd_le — Mathlib

English

Let α be a preorder. For all a,b in Multiplicative α, a ≤ b in Multiplicative α if and only if a.toAdd ≤ b.toAdd in α.

Русский

Пусть α упорядочено. Для любых a,b в Multiplicative α имеем: a ≤ b по этому порядку в Multiplicative α тогда и только тогда, когда a.toAdd ≤ b.toAdd в α.

LaTeX

$$$a \le b \iff a.toAdd \le b.toAdd$$$

Lean4

@[simp]
theorem toAdd_le {a b : Multiplicative α} : a.toAdd ≤ b.toAdd ↔ a ≤ b :=
  Iff.rfl

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