flip_quotDualCoannihilatorToDual_bijective

English

The flipped quotient-to-dual coannihilator map is bijective for finite-dimensional W.

Русский

Разворотная карта фактор-дуподобной коаннигиляторной дуальности биективна при конечной размерности W.

LaTeX

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

Lean4

theorem flip_quotDualCoannihilatorToDual_bijective (W : Subspace K (Dual K V)) [FiniteDimensional K W] :
    Function.Bijective W.quotDualCoannihilatorToDual.flip :=
  letI : AddCommGroup W := inferInstance
  flip_bijective_iff₂.mpr W.quotDualCoannihilatorToDual_bijective

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