isometry_map_mkMetric — Mathlib

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]

Похожие утверждения