add_le_of_forall_ne — Mathlib

English

If no smaller left-summand or right-summand yields a given target c, then a + b ≤ c.

Русский

Если ни одна меньшая левая сумма a' + b или правая сумма a + b' не даёт c, то a + b ≤ c.

LaTeX

$$$\\\\forall {a b c : \\\\mathrm{Nimber}},\\\\ (\\\\forall a' < a,\\\\ a' + b \\neq c) \\\\Rightarrow \\\\ (\\\\forall b' < b,\\\\ a + b' \\\\neq c) \\\\Rightarrow \\\\text{``}\\\\text{a} + \\\\text{b} \\\\le c\\\\text{''}.$$$

Lean4

theorem add_le_of_forall_ne (h₁ : ∀ a' < a, a' + b ≠ c) (h₂ : ∀ b' < b, a + b' ≠ c) : a + b ≤ c :=
  by
  by_contra! h
  have := exists_of_lt_add h
  tauto

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