dualSubmodule_flip_dualSubmodule_of_basis

English

For a finite basis b, the flipped dualSubmodule of the dualSubmodule of span b equals span b: B.flip.dualSubmodule(B.dualSubmodule(span_R(range b))) = span_R(range b).

Русский

Для конечного базиса b перевёрнутая дуальная подмодуля двойственной подмодуля span b даёт тот же подмодуль.

LaTeX

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

Lean4

theorem dualSubmodule_flip_dualSubmodule_of_basis {ι : Type*} [Finite ι] (hB : B.Nondegenerate) (b : Basis ι S M) :
    B.flip.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 _ hB.flip, dualBasis_flip_dualBasis B hB]

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