continuous

Mathlib.Analysis.Normed.Affine.Isometry

URI: https://scilib.ai/kg/mathlib#AffineIsometry.continuous

English

The diameter of the image of a set under an affine isometry equals the diameter of the set.

Русский

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

LaTeX

$$"EDiam"(f '' s) = "EDiam"(s)$$

Lean4

@[continuity]
protected theorem continuous : Continuous f :=
  f.isometry.continuous

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

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

Разделы

Аффилиация

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