dualMap_dualMap_eq_iff — Mathlib

English

Assume M is reflexive and Dual.eval on M' is bijective. Then f.dualMap.dualMap = g.dualMap.dualMap implies f = g for linear maps f,g: M → M'.

Русский

Пусть M рефлексивна, и для M' отображение двойственного оценивания биективно. Тогда из равенства f^{**} = g^{**} следует f = g для линейных отображений f,g: M → M'.

LaTeX

$$$\\operatorname{Bijective}(\\mathrm{Dual.eval}(R,M')) \\Rightarrow \\big( f^{**} = g^{**} \\iff f = g \\big).$$$

Lean4

@[simp]
theorem dualMap_dualMap_eq_iff {M' : Type*} [AddCommMonoid M'] [Module R M'] [IsReflexive R M'] {f g : M →ₗ[R] M'} :
    f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g :=
  dualMap_dualMap_eq_iff_of_injective _ _ (bijective_dual_eval R M').injective

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