metricSpace

Mathlib.Analysis.Normed.Unbundled.SpectralNorm

URI: https://scilib.ai/kg/mathlib#spectralNorm.metricSpace

← MathLib Explorer

English

The metric on L is defined by d(x,y) = spectralNorm(K,L)(x - y).

Русский

Метрика на L задаётся как d(x,y) = spectralNorm(K,L)(x - y).

LaTeX

$$$d(x,y) = \mathrm{spectralNorm}(K,L,x-y)$$$

Lean4

/-- The metric space structure on `L` induced by the spectral norm. -/
def metricSpace [CompleteSpace K] : MetricSpace L :=
  (normedField K L).toMetricSpace

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

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

Разделы

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

Аффилиация

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