dist_mkOfCompact — Mathlib

English

For α compact, the distance between mkOfCompact f and mkOfCompact g equals the distance between f and g.

Русский

Для компактного α расстояние между mkOfCompact f и mkOfCompact g равно расстоянию между f и g.

LaTeX

$$$\operatorname{dist}\bigl(\mathrm{mkOfCompact} f, \mathrm{mkOfCompact} g\bigr) = \operatorname{dist}(f,g)$$$

Lean4

@[simp]
theorem _root_.BoundedContinuousFunction.dist_mkOfCompact (f g : C(α, β)) :
    dist (mkOfCompact f) (mkOfCompact g) = dist f g :=
  rfl

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