exists_lt_add_of_lt_add — Mathlib

English

If x < y + z with y ≠ 0 and z ≠ 0, then there exist y' < y and z' < z such that x < y' + z'.

Русский

Если x < y + z и y ≠ 0, z ≠ 0, то найдутся y' < y и z' < z такие, что x < y' + z'.

LaTeX

$$$x < y + z \\;\\land\\; y \\neq 0 \\;\\land\\; z \\neq 0 \\Rightarrow \\exists y' < y, \\exists z' < z, x < y' + z'$$$

Lean4

theorem exists_lt_add_of_lt_add {x y z : ℝ≥0∞} (h : x < y + z) (hy : y ≠ 0) (hz : z ≠ 0) :
    ∃ y' < y, ∃ z' < z, x < y' + z' := by
  contrapose! h
  simpa using biSup_add_biSup_le' (by exact ⟨0, hy.bot_lt⟩) (by exact ⟨0, hz.bot_lt⟩) h

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