Commit 2026-06-10 10:22 22e4e692

View on Github →

refactor(Analysis/Normed/Module/Complemented): add IsCompl.isTopCompl_of_isClosed and isTopCompl_iff_isCompl_isClosed (#39815) Adds two theorems:

  • IsCompl.isTopCompl_of_isClosed: In a Banach space, two closed submodules that are algebraic complements are topological
  • isTopCompl_iff_isCompl_isClosed: p and q are topological complements if and only if p and q are algebraic complements and p and q are both closed. Additionally much of the ClosedCompl results are deprecated in favour of using TopCompl.

Estimated changes