diam_range

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometry.diam_range

English

Diameter of the range equals the diameter of the entire domain, under a semilinear isometry.

Русский

Диаметр образа диапазона равен диаметру всего пространства под полулинейкой изометрией.

LaTeX

$$ediam(range f) = ediam(univ)$$

Lean4

theorem diam_range : Metric.diam (range f) = Metric.diam (univ : Set E) :=
  Isometry.diam_range (LinearIsometry.isometry f)

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

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

Разделы

Аффилиация

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