lt_iff_exists_add_pos_lt — Mathlib

English

For ENNReal a < b, there exists r ≥ 0 with 0 < r and a + r < b.

Русский

Для a < b существует r ≥ 0 с 0 < r и a + r < b.

LaTeX

$$$ a < b \iff \exists r : \mathbb{R}_{\\ge 0}, 0 < r \land a + r < b $$$

Lean4

theorem lt_iff_exists_add_pos_lt : a < b ↔ ∃ r : ℝ≥0, 0 < r ∧ a + r < b :=
  by
  refine ⟨fun hab => ?_, fun ⟨r, _, hr⟩ => lt_of_le_of_lt le_self_add hr⟩
  rcases lt_iff_exists_nnreal_btwn.1 hab with ⟨c, ac, cb⟩
  lift a to ℝ≥0 using ac.ne_top
  rw [coe_lt_coe] at ac
  refine ⟨c - a, tsub_pos_iff_lt.2 ac, ?_⟩
  rwa [← coe_add, add_tsub_cancel_of_le ac.le]

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