quotDualCoannihilatorToDual_bijective

English

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

Русский

Картa фактор-дуального коаннигиляторa биективна для конечномерных подпространств.

LaTeX

$$W.quotDualCoannihilatorToDual bijective$$

Lean4

theorem quotDualCoannihilatorToDual_bijective (W : Subspace K (Dual K V)) [FiniteDimensional K W] :
    Function.Bijective W.quotDualCoannihilatorToDual :=
  ⟨W.quotDualCoannihilatorToDual_injective,
    letI : AddCommGroup W := inferInstance
    flip_injective_iff₂.mp W.flip_quotDualCoannihilatorToDual_injective⟩

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