English
When the reference set is dense, the embeddingOfSubset map is an isometry on its image.
Русский
Если опорный набор плотный, отображение embeddingOfSubset является изометрией на своем образе.
LaTeX
$$$\text{Isometry}(\mathrm{embeddingOfSubset} \ x)$$$
Lean4
/-- When the reference set is dense, the embedding map is an isometry on its image. -/
theorem embeddingOfSubset_isometry (H : DenseRange x) : Isometry (embeddingOfSubset x) :=
by
refine Isometry.of_dist_eq fun a b => ?_
refine
(embeddingOfSubset_dist_le x a b).antisymm
(le_of_forall_pos_le_add fun e epos => ?_)
-- First step: find n with dist a (x n) < e
rcases Metric.mem_closure_range_iff.1 (H a) (e / 2) (half_pos epos) with
⟨n, hn⟩
-- Second step: use the norm control at index n to conclude
have C : dist b (x n) - dist a (x n) = embeddingOfSubset x b n - embeddingOfSubset x a n := by
simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]
have :=
calc
dist a b ≤ dist a (x n) + dist (x n) b := dist_triangle _ _ _
_ = 2 * dist a (x n) + (dist b (x n) - dist a (x n)) := by simp [dist_comm]; ring
_ ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)| := by grw [← le_abs_self]
_ ≤ 2 * (e / 2) + |embeddingOfSubset x b n - embeddingOfSubset x a n| :=
by
rw [C]
gcongr
_ ≤ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) :=
by
gcongr
simp only [dist_eq_norm]
exact lp.norm_apply_le_norm ENNReal.top_ne_zero (embeddingOfSubset x b - embeddingOfSubset x a) n
_ = dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e := by ring
simpa [dist_comm] using this
