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]