English
If f is an isometry and either m is monotone or f is surjective, then comap f (mkMetric m) = mkMetric m.
Русский
Если f геометрически изометрично отображает X в Y и либо m монотонна, либо f сюръективен, то comap f (mkMetric m) = mkMetric m.
LaTeX
$$comap f (mkMetric m) = mkMetric m$$
Lean4
theorem isometry_comap_mkMetric (m : ℝ≥0∞ → ℝ≥0∞) {f : X → Y} (hf : Isometry f) (H : Monotone m ∨ Surjective f) :
comap f (mkMetric m) = mkMetric m :=
by
simp only [mkMetric, mkMetric', mkMetric'.pre, comap_iSup]
refine surjective_id.iSup_congr id fun ε => surjective_id.iSup_congr id fun hε => ?_
rw [comap_boundedBy _ (H.imp _ id)]
· congr with s : 1
apply extend_congr <;> simp [hf.ediam_image]
· intro h_mono s t hst
simp only [extend, le_iInf_iff]
intro ht
apply le_trans _ (h_mono (diam_mono hst))
simp only [(diam_mono hst).trans ht, le_refl, ciInf_pos]
