English
Let E be a normed real vector space. If hδ > 0, hε > 0 and dist(x,z) < ε+δ, 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 δ,ε ∈ ℝ,\ δ > 0,\ ε > 0,\ dist(x,z) < ε+δ \Rightarrow \exists y \in E:\ dist(x,y) < δ \land dist(y,z) < ε. $$$$
Lean4
theorem exists_dist_lt_lt (hδ : 0 < δ) (hε : 0 < ε) (h : dist x z < ε + δ) : ∃ y, dist x y < δ ∧ dist y z < ε :=
by
refine
(exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ.le) (div_nonneg hδ.le <| add_nonneg hε.le hδ.le) <| by
rw [← add_div, div_self (add_pos hε hδ).ne']).imp
fun y hy => ?_
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
rw [← div_lt_one (add_pos hε hδ)] at h
exact
⟨mul_lt_of_lt_one_left hδ h, mul_lt_of_lt_one_left hε h⟩
-- This is also true for `ℚ`-normed spaces
