eval_range — Mathlib

English

The range of the evaluation map Dual.eval R M is the whole target space; i.e., range(Dual.eval R M) = ⊤.

Русский

Образ отображения оценки Dual.eval R M равен всей цели; то есть range(Dual.eval R M) = ⊤.

LaTeX

$$$ \\mathrm{range}(\\mathrm{Dual.eval} \\; R\\; M) = \\top $$$

Lean4

theorem eval_range {ι : Type*} [Finite ι] (b : Basis ι R M) : LinearMap.range (Dual.eval R M) = ⊤ := by
  classical
  cases nonempty_fintype ι
  rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]

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