dualCopairing_nondegenerate — Mathlib

English

For a subspace W of V, the dual copairing on W is nondegenerate.

Русский

Для подпространства W ⊆ V дуальное копарирование невырождено.

LaTeX

$$$W_{\\text{dualCopairing}}\\;\\text{Nondegenerate}$$$

Lean4

theorem dualCopairing_nondegenerate (W : Subspace K V₁) : W.dualCopairing.Nondegenerate :=
  by
  constructor
  · rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualCopairing_eq]
    apply LinearEquiv.ker
  · rintro ⟨x⟩
    simp only [Quotient.quot_mk_eq_mk, dualCopairing_apply, Quotient.mk_eq_zero]
    rw [← forall_mem_dualAnnihilator_apply_eq_zero_iff, SetLike.forall]
    exact id

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