English
If V is finite-dimensional over K, then the map W ↦ W⊥ gives an antitone bijection between the lattice of subspaces of V and the lattice of subspaces of V*, with inverse U ↦ U⊥.
Русский
Если V конечномерно над полем K, существует антиоднозначное соответствие между подпространствами V и подпространствами V*, заданное W ↦ W⊥ и обратное U ↦ U⊥.
LaTeX
$$$$[\\text{FinDim } V] \\quad\\Rightarrow\\quad \\operatorname{Sub}(V) \\cong_o \\operatorname{Sub}(V^*)^{op},\\quad W \\mapsto W^{\\perp},\\ U \\mapsto U^{\\perp}.$$$$
Lean4
/-- For any finite-dimensional vector space, `dualAnnihilator` and `dualCoannihilator` give
an antitone order isomorphism between the subspaces in the vector space and the subspaces
in its dual. -/
def orderIsoFiniteDimensional [FiniteDimensional K V] : Subspace K V ≃o (Subspace K (Dual K V))ᵒᵈ
where
toFun W := toDual W.dualAnnihilator
invFun W := (ofDual W).dualCoannihilator
left_inv _ := dualAnnihilator_dualCoannihilator_eq
right_inv _ := dualCoannihilator_dualAnnihilator_eq
map_rel_iff' := dualAnnihilator_le_dualAnnihilator_iff
