Operations on extended real numbers

This file supplements Mathlib's API for arithmetic operations on EReal. The common theme is subtraction in which one operand is a real number: both a - (r : EReal) and (r : EReal) - a are defined for every extended real a, are never of the form ∞ - ∞, and behave like real subtraction in the ways recorded here. The first two results below have a real subtrahend and the last two a real minuend.

Main results

• EReal.iInf_sub_coe and EReal.iSup_sub_coe — subtracting a real constant commutes with an infimum and with a supremum in EReal;
• EReal.coe_sub_add_coe — subtracting a sum whose final term is real can be reassociated when the minuend is real;
• EReal.coe_sub_le_comm — the two subtrahends of a real minuend can be exchanged across an inequality, as in sub_le_comm for groups;
• EReal.neg_sub_coe and EReal.neg_coe_sub — negating a difference with one real operand exchanges the operands, with no finiteness hypothesis on the other;
• EReal.sub_sub_coe_eq_add_coe_sub and EReal.sub_coe_add_eq_add_sub — a real subtrahend moves freely through sums and differences, as in sub_sub_eq_add_sub and sub_add_eq_add_sub for groups;
• EReal.sub_coe_eq_iff_eq_add_coe — a real subtrahend can be moved across an equation, as in sub_eq_iff_eq_add for groups;
• EReal.add_eq_coe_iff_neg_add_neg_eq — an equation between a sum and a real number can be negated term by term.

theorem EReal.iInf_sub_coe {ι : Sort u_1} (f : ι → EReal) (a : ℝ) : ⨅ (i : ι), f i - ↑a = (⨅ (i : ι), f i) - ↑a

Subtracting a real constant commutes with an infimum in EReal; both sides are ⊤ when the index type is empty.

theorem EReal.iSup_sub_coe {ι : Sort u_1} (f : ι → EReal) (a : ℝ) : ⨆ (i : ι), f i - ↑a = (⨆ (i : ι), f i) - ↑a

Subtracting a real constant commutes with a supremum in EReal; both sides are ⊥ when the index type is empty.

theorem EReal.coe_sub_add_coe (b : EReal) (d a : ℝ) : ↑d - (b + ↑a) = ↑d - b - ↑a

Subtracting a sum whose final term is real can be reassociated when the minuend is real.

theorem EReal.coe_sub_le_comm {r : ℝ} {a b : EReal} : ↑r - a ≤ b ↔ ↑r - b ≤ a

With a real minuend, the subtrahend and the right-hand side of an inequality can be exchanged: r - a ≤ b ↔ r - b ≤ a. This is sub_le_comm for EReal, and it holds with no finiteness hypothesis on a or b.

theorem EReal.neg_sub_coe (b : EReal) (r : ℝ) : -(b - ↑r) = ↑r - b

Negating a difference with a real subtrahend exchanges the operands, for every extended-real minuend.

theorem EReal.neg_coe_sub (r : ℝ) (b : EReal) : -(↑r - b) = b - ↑r

Negating a difference with a real minuend exchanges the operands, for every extended-real subtrahend.

theorem EReal.sub_sub_coe_eq_add_coe_sub (x y : EReal) (a : ℝ) : x - (y - ↑a) = x + ↑a - y

A real subtrahend inside a subtrahend can be pulled out as a summand, for all extended-real x and y: this is sub_sub_eq_add_sub for EReal, with no finiteness hypothesis.

theorem EReal.sub_coe_add_eq_add_sub (x y : EReal) (a : ℝ) : x - ↑a + y = x + y - ↑a

A real subtrahend commutes past a summand, for all extended-real x and y: this is sub_add_eq_add_sub for EReal, with no finiteness hypothesis.

theorem EReal.sub_coe_eq_iff_eq_add_coe {x y : EReal} {a : ℝ} : x - ↑a = y ↔ x = y + ↑a

A real subtrahend can be moved across an equation in EReal, for all extended-real x and y: this is sub_eq_iff_eq_add for EReal, with no finiteness hypothesis.

theorem EReal.add_eq_coe_iff_neg_add_neg_eq {x y : EReal} {r : ℝ} : x + y = ↑r ↔ -x + -y = ↑(-r)

An equation between a sum of extended reals and a real number can be negated term by term. Both sides force x and y to be real, so no finiteness hypothesis is needed, even though -(x + y) = -x + -y fails in EReal when x and y are opposite infinities.