Projection onto a ray in an ordered group #
This file shows that in a linearly ordered additive group the distance of Set.projIci a x above
a is the positive part of x - a, the difference when x lies above a and zero otherwise. It
is an [UPSTREAM] addition to Mathlib.Algebra.Order.Interval.Set.Group.
theorem
Set.coe_projIci_sub
{α : Type u_1}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
(a x : α)
:
↑(projIci a x) - a = (x - a)⁺