exists_of_lt_add — Mathlib

English

If c < a + b, then either there exists a' < a with a' + b = c or there exists b' < b with a + b' = c.

Русский

Если c < a + b, то существует либо a' < a такой, что a' + b = c, либо b' < b такой, что a + b' = c.

LaTeX

$$$\\\\forall {a b c : \\\\mathrm{Nimber}},\\\\ c < a + b \\\\Rightarrow \\\\exists a' < a, a' + b = c \\\\lor \\\\exists b' < b, a + b' = c.$$$

Lean4

theorem exists_of_lt_add (h : c < a + b) : (∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c :=
  by
  rw [add_def] at h
  have := notMem_of_lt_csInf' h
  rwa [Set.mem_compl_iff, not_not] at this

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