Commit 2020-08-19 13:32 15cacf0e
View on Github →feat(analysis/normed_space/real_inner_product): orthogonal subspace order (#3863)
Define the Galois connection between submodule ℝ α and its
order_dual given by submodule.orthogonal. Thus, deduce that the
inf of orthogonal subspaces is the subspace orthogonal to the sup (for
three different forms of inf), as well as replacing the proof of
submodule.le_orthogonal_orthogonal by a use of
galois_connection.le_u_l.