dualPairing_nondegenerate — Mathlib

English

For any subspace W ⊆ V, the dual pairing on W is nondegenerate.

Русский

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

LaTeX

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

Lean4

theorem dualPairing_nondegenerate (W : Subspace K V₁) : W.dualPairing.Nondegenerate :=
  by
  constructor
  · rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualPairing_eq]
    apply LinearEquiv.ker
  · intro x h
    rw [← forall_dual_apply_eq_zero_iff K x]
    intro φ
    simpa only [Submodule.dualPairing_apply, dualLift_of_subtype] using h (Submodule.Quotient.mk (W.dualLift φ))

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