Theorems · Theorem · order theory

lt_iff_exists_add

∀ {α : Type u} [inst : AddZeroClass α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] {a b : α}
  [AddLeftStrictMono α], a < b ↔ ∃ c > 0, b = a + c

Defined in

Mathlib.Algebra.Order.Monoid.Canonical.Defs

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext, Quot.sound

Assumes

AddZeroClassPartialOrderCanonicallyOrderedAddAddLeftStrictMono