sub_add_eq_add_sub — Mathlib

English

If b ≤ a and b ≠ ∞, then a − b + c = a + c − b (with a special case when c = ∞).

Русский

Если b ≤ a и b ≠ ∞, то a − b + c = a + c − b (в отдельном случае c = ∞ выступает отдельно).

LaTeX

$$$$ \text{If } b \le a \text{ and } b \neq \infty, \; a - b + c = a + c - b. $$$$

Lean4

protected theorem sub_add_eq_add_sub (hab : b ≤ a) (b_ne_top : b ≠ ∞) : a - b + c = a + c - b :=
  by
  by_cases c_top : c = ∞
  · simpa [c_top] using ENNReal.eq_sub_of_add_eq b_ne_top rfl
  refine ENNReal.eq_sub_of_add_eq b_ne_top ?_
  simp only [add_assoc, add_comm c b]
  simpa only [← add_assoc] using (add_left_inj c_top).mpr <| tsub_add_cancel_of_le hab

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