toStrongDual_apply

Mathlib.Analysis.Normed.Module.WeakDual

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

English

The map toStrongDual is injective on WeakDual 𝕜 E; hence equals its inverse on its image.

Русский

Отображение toStrongDual инъективно на WeakDual 𝕜 E; следовательно, равно своей обратной на образе.

LaTeX

$$$ toStrongDual\\;: WeakDual\\; 𝕜 E \\to StrongDual\\; 𝕜 E \\text{ is injective}$$$

Lean4

theorem toStrongDual_apply (x : WeakDual 𝕜 E) (y : E) : (toStrongDual x) y = x y :=
  rfl

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

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

Разделы

Аффилиация

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