Theorem Submodule.isTopCompl_iff_isCompl_isClosed

Modification history

2026-06-10 10:22
Mathlib/Analysis/Normed/Module/Complemented.lean
refactor(Analysis/Normed/Module/Complemented): add `IsCompl.isTopCompl_of_isClosed` and `isTopCompl_iff_isCompl_isClosed` (#39815) …
Added Submodule.isTopCompl_iff_isCompl_isClosedView on Github →