Theorem Submodule.IsCompl.isTopCompl_of_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.IsCompl.isTopCompl_of_isClosed View on Github →