Commit 2025-06-10 13:25 5bc4d646

View on Github →

feat(Analysis/InnerProductSpace/Projection): add lemma Submodule.le_iff_orthogonal_le_orthogonal and similars (#25240)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

added theorem Submodule.le_orthogonal_iff_le_orthogonal

added theorem Submodule.orthogonal_le_iff_orthogonal_le

added theorem Submodule.orthogonal_le_orthogonal_iff