English
If f: X → Y is an isometry and m: ℝ≥0∞ → ℝ≥0∞, then map f (mkMetric m) = restrict (range f) (mkMetric m) provided Monotone m or Surjective f.
Русский
Пусть f: X → Y есть изометрия и m: ℝ≥0∞ → ℝ≥0∞. Тогда перенос measure через f равен ограничению mkMetric m на образе f, при условии монотонности m или сюржективности f.
LaTeX
$$$ map f (mkMetric m) = \operatorname{restrict} (\operatorname{range} f) (mkMetric m) $$$
Lean4
theorem isometry_map_mkMetric (m : ℝ≥0∞ → ℝ≥0∞) {f : X → Y} (hf : Isometry f) (H : Monotone m ∨ Surjective f) :
map f (mkMetric m) = restrict (range f) (mkMetric m) := by rw [← isometry_comap_mkMetric _ hf H, map_comap]