sub_right_inj — Mathlib

English

If a ≠ ∞, b ≤ a, c ≤ a, then a − b = a − c iff b = c.

Русский

Если a ≠ ∞, b ≤ a, c ≤ a, то a − b = a − c тогда и только если b = c.

LaTeX

$$$ (ha: a \neq \infty) \land (hb: b \le a) \land (hc: c \le a) \Rightarrow a - b = a - c \iff b = c $$$

Lean4

theorem sub_right_inj {a b c : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≤ a) (hc : c ≤ a) : a - b = a - c ↔ b = c :=
  (cancel_of_ne ha).tsub_right_inj (cancel_of_ne <| ne_top_of_le_ne_top ha hb)
    (cancel_of_ne <| ne_top_of_le_ne_top ha hc) hb hc

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