id_toContinuousLinearMap

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The toContinuousLinearMap construction is injective: it preserves equality of isometries.

Русский

Конструкция toContinuousLinearMap инъективна: она сохраняет равенство изометрий.

LaTeX

$$toContinuousLinearMap_injective : Function.Injective (toContinuousLinearMap)$$

Lean4

@[simp]
theorem id_toContinuousLinearMap : id.toContinuousLinearMap = ContinuousLinearMap.id R E :=
  rfl

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

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

Разделы

Аффилиация

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