English
Let E be a normed real vector space. For x,z ∈ E and δ,ε ∈ ℝ with δ ≥ 0 and ε ≥ 0, if dist(x,z) ≤ ε+δ, then there exists y ∈ E with dist(x,y) ≤ δ and dist(y,z) ≤ ε.
Русский
Пусть E — нормированное вещественное векторное пространство. Пусть x,z ∈ E и δ,ε ∈ ℝ с δ ≥ 0, ε ≥ 0. Если dist(x,z) ≤ ε+δ, то существует y ∈ E такое, что dist(x,y) ≤ δ и dist(y,z) ≤ ε.
LaTeX
$$$$\forall x,z \in E,\forall δ,ε \in \mathbb{R}_{\ge 0},\ dist(x,z) \le ε+δ \Rightarrow \exists y \in E:\ dist(x,y) \le δ \land dist(y,z) \le ε. $$$$
Lean4
theorem exists_dist_le_le (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (h : dist x z ≤ ε + δ) : ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε :=
by
obtain rfl | hε' := hε.eq_or_lt
· exact ⟨z, by rwa [zero_add] at h, (dist_self _).le⟩
have hεδ := add_pos_of_pos_of_nonneg hε' hδ
refine
(exists_dist_eq x z (div_nonneg hε <| add_nonneg hε hδ) (div_nonneg hδ <| add_nonneg hε hδ) <| by
rw [← add_div, div_self hεδ.ne']).imp
fun y hy => ?_
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
rw [← div_le_one hεδ] at h
exact
⟨mul_le_of_le_one_left hδ h, mul_le_of_le_one_left hε h⟩
-- This is also true for `ℚ`-normed spaces
