isometry_ofReal

Mathlib.Analysis.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.isometry_ofReal

English

The map ℝ → ℂ given by x ↦ x is an isometry.

Русский

Отображение x ↦ x из ℝ в ℂ сохраняет расстояния.

LaTeX

$$$\\\\operatorname{dist}(\\\\operatorname{ofReal}(x), \\\\operatorname{ofReal}(y)) = \\\\operatorname{dist}(x,y)$$$

Lean4

theorem isometry_ofReal : Isometry ((↑) : ℝ → ℂ) :=
  ofRealLI.isometry

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

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

Разделы

Аффилиация

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