English
For a finite-dimensional vector space V over K, the natural pairing between V and its dual V* is nondegenerate: if a vector x ≠ 0, there exists a functional φ with φ(x) ≠ 0, and conversely for φ ≠ 0 there exists x with φ(x) ≠ 0.
Русский
Для конечномерного пространства V над K естественное дуальное парирование между V и его дуальным пространством V* не вырождено: для любого ненулевого вектора существует функционал, действующий на него ненулево, и наоборот.
LaTeX
$$$\\text{Dual pairing } \\langle \\cdot, \\cdot \\rangle: V \\times V^* \\to K\\; \\text{ is nondegenerate, i.e. } \\\\ (\\forall x \\in V \\setminus \\{0\\}, \\exists \\phi \\in V^*:\\; \\phi(x) \\neq 0) \\land (\\forall \\phi \\in V^* \\setminus \\{0\\}, \\exists x \\in V:\\; \\phi(x) \\neq 0).$$$
Lean4
theorem dualPairing_nondegenerate : (dualPairing K V₁).Nondegenerate :=
⟨separatingLeft_iff_ker_eq_bot.mpr ker_id, fun x => (forall_dual_apply_eq_zero_iff K x).mp⟩
