Theorems · Definition · order theory

AddLECancellable

{α : Type u_1} → [Add α] → [LE α] → α → Prop

An element a : α is AddLECancellable if x ↦ a + x is order-reflecting. We will make a separate version of many lemmas that require [MulLeftReflectLE α] with AddLECancellable assumptions instead. These lemmas can then be instantiated to specific types, like ENNReal, where we can replace the assumption AddLECancellable x by x ≠ ∞.

Defined in

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Cited by

87 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

AddLE