toAdd_lt — 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 по мультипликативному порядку тогда и только тогда, когда a.toAdd < b.toAdd в α.

LaTeX

$$$a \lt b \iff a.toAdd \lt b.toAdd$$$

Lean4

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

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