mathlib3

15cacf0e - feat(analysis/normed_space/real_inner_product): orthogonal subspace order (#3863)

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`.