dualCoannihilator_dualAnnihilator_eq

English

The flipped map (Submodule.quotDualCoannihilatorToDual).flip is bijective for finite-dimensional W.

Русский

Разворотная карта (Submodule.quotDualCoannihilatorToDual).flip биективна при конечной размерности W.

LaTeX

$$Function.Bijective (Submodule.quotDualCoannihilatorToDual W).flip$$

Lean4

theorem dualCoannihilator_dualAnnihilator_eq {W : Subspace K (Dual K V)} [FiniteDimensional K W] :
    W.dualCoannihilator.dualAnnihilator = W :=
  let e :=
    (LinearEquiv.ofBijective _ W.flip_quotDualCoannihilatorToDual_bijective).trans
      (Submodule.dualQuotEquivDualAnnihilator _)
  letI : AddCommGroup W := inferInstance
  haveI : FiniteDimensional K W.dualCoannihilator.dualAnnihilator := LinearEquiv.finiteDimensional e
  (eq_of_le_of_finrank_eq W.le_dualCoannihilator_dualAnnihilator e.finrank_eq).symm

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