toDual_range — Mathlib

English

The range of the map toDual is the entire dual space: range(b.toDual) = ⊤.

Русский

Область значения отображения toDual равна все дуальное пространство: range(b.toDual) = ⊤.

LaTeX

$$$ \operatorname{range}(b.toDual) = \top. $$$

Lean4

theorem toDual_range [Finite ι] : LinearMap.range b.toDual = ⊤ :=
  by
  refine eq_top_iff'.2 fun f => ?_
  refine ⟨Finsupp.linearCombination R b (Finsupp.equivFunOnFinite.symm fun i => f (b i)), b.ext fun i => ?_⟩
  rw [b.toDual_eq_repr _ i, repr_linearCombination b, Finsupp.equivFunOnFinite_symm_apply_toFun]

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