isometry

Mathlib.Analysis.Normed.Affine.Isometry

URI: https://scilib.ai/kg/mathlib#AffineIsometryEquiv.isometry

English

An affine isometry equivalence is a continuous map.

Русский

Аффинная изометрия-эквивалент непрерывна.

LaTeX

$$$$ \text{Continuous}(e) \quad\text{for } e : P \simeq^{\mathrm{AI}} P_2. $$$$

Lean4

protected theorem isometry : Isometry e :=
  e.toAffineIsometry.isometry

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

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

Разделы

Аффилиация

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