English
Let E be a normed real vector space. If hδ > 0, hε ≥ 0 and dist(x,z) < ε+δ, then there exists y ∈ E with dist(x,y) < δ and dist(y,z) ≤ ε.
Русский
Пусть E — нормированное вещественное векторное пространство. Пусть hδ > 0, hε ≥ 0 и dist(x,z) < ε+δ. Тогда существует y ∈ E такое, что dist(x,y) < δ и dist(y,z) ≤ ε.
LaTeX
$$$$\forall x,z \in E,\forall δ,ε \in \mathbb{R},\ δ > 0,\ ε \ge 0,\ dist(x,z) < ε+δ \Rightarrow \exists y \in E:\ dist(x,y) < δ \land dist(y,z) \le ε. $$$$
Lean4
theorem exists_dist_lt_le (hδ : 0 < δ) (hε : 0 ≤ ε) (h : dist x z < ε + δ) : ∃ y, dist x y < δ ∧ dist y z ≤ ε :=
by
obtain ⟨y, yz, xy⟩ := exists_dist_le_lt hε hδ (show dist z x < δ + ε by simpa only [dist_comm, add_comm] using h)
exact
⟨y, by simp [dist_comm x y, dist_comm y z, *]⟩
-- This is also true for `ℚ`-normed spaces
