mkMetric_mono — Mathlib

English

For an isometry equivalence f: X ≃ᵢ Y, comap (EquivLike.toFunLike.coe f) (mkMetric m) = mkMetric m.

Русский

Для изометрического эквивалента f: X ≃ᵢ Y верно comap (коэрц f) (mkMetric m) = mkMetric m.

LaTeX

$$$ comap f (mkMetric m) = mkMetric m $$$

Lean4

/-- If `m₁ d ≤ m₂ d` for `d < ε` for some `ε > 0` (we use `≤ᶠ[𝓝[≥] 0]` to state this), then
`mkMetric m₁ hm₁ ≤ mkMetric m₂ hm₂`. -/
theorem mkMetric_mono {m₁ m₂ : ℝ≥0∞ → ℝ≥0∞} (hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂) : (mkMetric m₁ : Measure X) ≤ mkMetric m₂ := by
  convert @mkMetric_mono_smul X _ _ _ _ m₂ _ ENNReal.one_ne_top one_ne_zero _ <;> simp [*]

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