Commit 2026-05-05 09:37 84637434

View on Github →

feat: define Submodule.IsTopCompl (#38547) Right now, Mathlib defines Submodule.ClosedComplemented. Submodule.IsTopCompl is the more precise version saying that two subspaces are topological complements to each other.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Module/Complemented.lean

Modified Mathlib/Analysis/Normed/Module/ContinuousInverse.lean

Modified Mathlib/Analysis/Normed/Module/HahnBanach.lean

Modified Mathlib/LinearAlgebra/Projection.lean

added theorem Submodule.IsCompl.projection_add_projection_eq_id

added theorem Submodule.IsCompl.projection_apply_right

added theorem Submodule.IsCompl.projection_eq_id_sub_projection

Created Mathlib/Topology/Algebra/Module/Complement.lean

added theorem ContinuousLinearMap.IsIdempotentElem.eq_projectionL

added theorem ContinuousLinearMap.IsIdempotentElem.isTopCompl

added theorem ContinuousLinearMap.closedComplemented_ker_of_rightInverse

added theorem ContinuousLinearMap.closedComplemented_range_of_leftInverse

added theorem ContinuousLinearMap.isIdempotentElem_iff_eq_projectionL_range_ker

added theorem ContinuousLinearMap.isTopCompl_of_proj

added theorem ContinuousLinearMap.isTopCompl_range_ker_of_leftInverse

added theorem Submodule.ClosedComplemented.exists_isClosed_isCompl

added theorem Submodule.ClosedComplemented.exists_isTopCompl

added theorem Submodule.ClosedComplemented.exists_submodule_equiv_prod

added theorem Submodule.ClosedComplemented.isClosed_complement

added theorem Submodule.ClosedComplemented.isCompl_complement

added theorem Submodule.ClosedComplemented.isTopCompl_complement

added def Submodule.ClosedComplemented

added theorem Submodule.IsCompl.isTopCompl_iff

added theorem Submodule.IsCompl.isTopCompl_iff_linearProjOfIsCompl

added theorem Submodule.IsTopCompl.closedComplemented

added theorem Submodule.IsTopCompl.continuous_linearProjOfIsCompl

added theorem Submodule.IsTopCompl.isClosed'

added structure Submodule.IsTopCompl

added theorem Submodule.closedComplemented_bot

added theorem Submodule.closedComplemented_iff_exists_isTopCompl

added theorem Submodule.closedComplemented_top

added theorem Submodule.coe_projectionOntoL_apply

added theorem Submodule.isIdempotentElem_projectionL

added theorem Submodule.isQuotientMap_projectionOntoL

added theorem Submodule.isTopCompl_bot_top

added theorem Submodule.isTopCompl_top_bot

added theorem Submodule.ker_projectionL

added theorem Submodule.ker_projectionOntoL

added theorem Submodule.projectionL_add_projectionL_eq_id

added theorem Submodule.projectionL_add_projectionL_eq_self

added theorem Submodule.projectionL_apply

added theorem Submodule.projectionL_apply_eq_zero_iff

added theorem Submodule.projectionL_apply_left

added theorem Submodule.projectionL_apply_mem

added theorem Submodule.projectionL_apply_right

added theorem Submodule.projectionL_eq_id_sub_projectionL

added theorem Submodule.projectionL_eq_self_iff

added theorem Submodule.projectionL_eq_self_sub_projectionL

added theorem Submodule.projectionOntoL_apply_eq_zero_iff

added theorem Submodule.projectionOntoL_apply_left

added theorem Submodule.projectionOntoL_apply_right

added theorem Submodule.projectionOntoL_surjective

added theorem Submodule.range_projectionL

added theorem Submodule.range_projectionOntoL

added theorem Submodule.toLinearMap_projectionL

added theorem Submodule.toLinearMap_projectionOntoL

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

deleted theorem Submodule.ClosedComplemented.exists_submodule_equiv_prod

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

deleted theorem ContinuousLinearMap.closedComplemented_ker_of_rightInverse

deleted theorem Submodule.ClosedComplemented.exists_isClosed_isCompl

deleted theorem Submodule.ClosedComplemented.isClosed_complement

deleted theorem Submodule.ClosedComplemented.isCompl_complement

deleted def Submodule.ClosedComplemented

deleted theorem Submodule.closedComplemented_bot

deleted theorem Submodule.closedComplemented_top