toContinuousLinearEquiv_inj

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometryEquiv.toContinuousLinearEquiv_inj

← MathLib Explorer

English

The map toContinuousLinearEquiv is injective.

Русский

Отображение к toContinuousLinearEquiv инъективно.

LaTeX

$$$\mathrm{Injective}\big(\mathrm{toContinuousLinearEquiv}: _ \to E \simeq_{\sigma} E_2\big)$$$

Lean4

@[simp]
theorem toContinuousLinearEquiv_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
    f.toContinuousLinearEquiv = g.toContinuousLinearEquiv ↔ f = g :=
  toContinuousLinearEquiv_injective.eq_iff

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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