Commit 2023-12-04 13:54 19096ec3

View on Github →

chore(NormedSpace/Complemented): review API (#8596)

use And instead of Exists;
move lemmas from Subspace to Submodule namespace;
rename some lemmas to enable dot notation;
add ClosedComplemented.exists_submodule_equiv_prod.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Complemented.lean

added theorem Submodule.ClosedComplemented.of_isCompl_isClosed

added theorem Submodule.ClosedComplemented.of_quotient_finiteDimensional

added theorem Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl

added theorem Submodule.coe_continuous_linearProjOfClosedCompl'

added theorem Submodule.coe_continuous_linearProjOfClosedCompl

added theorem Submodule.coe_prodEquivOfClosedCompl

added theorem Submodule.coe_prodEquivOfClosedCompl_symm

added def Submodule.linearProjOfClosedCompl

added def Submodule.prodEquivOfClosedCompl

deleted theorem Subspace.closedComplemented_iff_has_closed_compl

deleted theorem Subspace.closedComplemented_of_closed_compl

deleted theorem Subspace.closedComplemented_of_quotient_finiteDimensional

deleted theorem Subspace.coe_continuous_linearProjOfClosedCompl'

deleted theorem Subspace.coe_continuous_linearProjOfClosedCompl

deleted theorem Subspace.coe_prodEquivOfClosedCompl

deleted theorem Subspace.coe_prodEquivOfClosedCompl_symm

deleted def Subspace.linearProjOfClosedCompl

deleted def Subspace.prodEquivOfClosedCompl

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

added theorem Submodule.ClosedComplemented.exists_isClosed_isCompl

added theorem Submodule.ClosedComplemented.exists_submodule_equiv_prod

deleted theorem Submodule.ClosedComplemented.has_closed_complement