dualSubmodule_dualSubmodule_of_basis

English

If B is nondegenerate and hB' is symmetry, then for any basis b, B.dualSubmodule( B.dualSubmodule(span_R(range b)) ) = span_R(range b).

Русский

Если B нондеґенеративна и hB' — симметрия, то для любого базиса b выполняется B.dualSubmodule( B.dualSubmodule(span_R(range b)) ) = span_R(range b).

LaTeX

$$$$ B.dualSubmodule(B.dualSubmodule(\mathrm{span}_R(\mathrm{range}\, b))) = \mathrm{span}_R(\mathrm{range}\, b). $$$$

Lean4

theorem dualSubmodule_dualSubmodule_of_basis {ι} [Finite ι] (hB : B.Nondegenerate) (hB' : B.IsSymm) (b : Basis ι S M) :
    B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range b))) = Submodule.span R (Set.range b) := by
  classical
  letI := FiniteDimensional.of_fintype_basis b
  rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB, dualBasis_dualBasis B hB hB']

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