instSeminormedAddCommGroup — Mathlib

English

The metric on C(α,E) satisfies dist(f,g) = ‖f − g‖, i.e., distance between two maps equals the norm of their difference.

Русский

Расстояние между двумя отображениями f,g в C(α,E) равно норме их разности: dist(f,g) = ‖f − g‖.

LaTeX

$$$\operatorname{dist}(f,g) = \|f - g\|$$$

Lean4

instance : SeminormedAddCommGroup C(α, E)
    where
  __ := ContinuousMap.instPseudoMetricSpace _ _
  __ := ContinuousMap.instAddCommGroupContinuousMap
  dist_eq x y := by rw [← norm_mkOfCompact, ← dist_mkOfCompact, dist_eq_norm, mkOfCompact_sub]
  dist := dist
  norm := norm

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