dualRestrict_surjective — Mathlib

English

The restriction map W.dualRestrict: V** → W* is surjective; every functional on W is a restriction of some functional on V.

Русский

Ограничивающее отображение W.dualRestrict: V** → W* сюръективно; каждому функционалу на W соответствует ограничение от некоторого функционала на V.

LaTeX

$$surjective( W.dualRestrict )$$

Lean4

theorem dualRestrict_surjective : Function.Surjective W.dualRestrict :=
  W.dualLift_rightInverse.surjective

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