toStrongDual_inj

Mathlib.Analysis.Normed.Module.WeakDual

URI: https://scilib.ai/kg/mathlib#WeakDual.toStrongDual_inj

← MathLib Explorer

English

For any nonzero x ∈ E and h: x ≠ 0, coord 𝕜 x h applied to x (viewed as 𝕜·x) equals 1.

Русский

Для ненулевого x вычисление coord 𝕜 x h на x (раcсматриваемом как 𝕜·x) даёт 1.

LaTeX

$$$$ coord\\, 𝕜\\, x\\, h (x) = 1 $$$$

Lean4

@[simp]
theorem toStrongDual_inj (x' y' : WeakDual 𝕜 E) : toStrongDual x' = toStrongDual y' ↔ x' = y' :=
  (LinearEquiv.injective toStrongDual).eq_iff

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

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

Разделы

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

Аффилиация

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