sub_le_of_le_add — Mathlib

English

If a ≤ b + c then a - c ≤ b.

Русский

Если a ≤ b + c, то a − c ≤ b.

LaTeX

$$$\forall a,b,c \in \mathrm{EReal},\ h:\ a \le b + c \Rightarrow a - c \le b$$$

Lean4

theorem sub_le_of_le_add {a b c : EReal} (h : a ≤ b + c) : a - c ≤ b := by
  induction c with
  | bot => rw [add_bot, le_bot_iff] at h; simp only [h, bot_sub, bot_le]
  | coe c => exact (sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h
  | top => simp only [sub_top, bot_le]

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