flip_quotDualCoannihilatorToDual_injective

English

Alternative formulation: the flip map is injective as a linear map on the dual coannihilator.

Русский

Альтернативная формулировка: перевёрнутое отображение является инъективным как линейное отображение на дуальной коаннигиляторе.

LaTeX

$$Injective(W.quotDualCoannihilatorToDual.flip)$$

Lean4

theorem flip_quotDualCoannihilatorToDual_injective (W : Submodule R (Dual R M)) :
    Function.Injective W.quotDualCoannihilatorToDual.flip := fun _ _ he ↦
  Subtype.ext <| LinearMap.ext fun m ↦ DFunLike.congr_fun he ⟦m⟧

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