Commit 2023-05-20 10:39 c9bcb0af

View on Github →

feat: port Analysis.NormedSpace.Complemented (#4131)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Complemented.lean

added theorem ContinuousLinearMap.coe_equivProdOfSurjectiveOfIsCompl

added theorem ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_apply

added theorem ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_toLinearEquiv

added theorem ContinuousLinearMap.ker_closedComplemented_of_finiteDimensional_range

added theorem Subspace.closedComplemented_iff_has_closed_compl

added theorem Subspace.closedComplemented_of_closed_compl

added theorem Subspace.closedComplemented_of_quotient_finiteDimensional

added theorem Subspace.coe_continuous_linearProjOfClosedCompl'

added theorem Subspace.coe_continuous_linearProjOfClosedCompl

added theorem Subspace.coe_prodEquivOfClosedCompl

added theorem Subspace.coe_prodEquivOfClosedCompl_symm

added def Subspace.linearProjOfClosedCompl

added def Subspace.prodEquivOfClosedCompl