English
Given a linear equivalence e: M ≃_R N, the target N is reflexive: IsReflexive(R,N).
Русский
Для линейного эквивалентного отображения e: M ≃_R N, пространство N рефлексивно: IsReflexive(R,N).
LaTeX
$$∀ e: M ≃_R N, IsReflexive(R,N).$$
Lean4
theorem equiv (e : M ≃ₗ[R] N) : IsReflexive R N where
bijective_dual_eval' :=
by
let ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
have : Dual.eval R N = ed.symm.comp ((Dual.eval R M).comp e.symm.toLinearMap) :=
by
ext m f
exact DFunLike.congr_arg f (e.apply_symm_apply m).symm
simp only [this, coe_comp, LinearEquiv.coe_coe, EquivLike.comp_bijective]
exact Bijective.comp (bijective_dual_eval R M) (LinearEquiv.bijective _)
