dist_eq_iSup

Mathlib.Topology.ContinuousMap.Compact

URI: https://scilib.ai/kg/mathlib#ContinuousMap.dist_eq_iSup

← MathLib Explorer

English

The distance between f and g equals the supremum over x of dist(f(x), g(x)).

Русский

Расстояние между f и g равно Sup_x dist(f(x), g(x)).

LaTeX

$$$\mathrm{dist}\, f g = \sup_{x} \mathrm{dist}(f(x), g(x))$$$

Lean4

theorem dist_eq_iSup : dist f g = ⨆ x, dist (f x) (g x) := by
  simp [← isometryEquivBoundedOfCompact α β |>.dist_eq f g, BoundedContinuousFunction.dist_eq_iSup]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru