Commit 2023-03-23 16:06 e11a7991

View on Github →

feat: port Analysis.NormedSpace.MStructure (#2915) port Analysis.NormedSpace.MStructure

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/MStructure.lean

added theorem IsLprojection.Lcomplement

added theorem IsLprojection.Lcomplement_iff

added theorem IsLprojection.coe_bot

added theorem IsLprojection.coe_compl

added theorem IsLprojection.coe_inf

added theorem IsLprojection.coe_one

added theorem IsLprojection.coe_sdiff

added theorem IsLprojection.coe_sup

added theorem IsLprojection.coe_top

added theorem IsLprojection.coe_zero

added theorem IsLprojection.commute

added theorem IsLprojection.compl_mul

added theorem IsLprojection.distrib_lattice_lemma

added theorem IsLprojection.join

added theorem IsLprojection.le_def

added theorem IsLprojection.mul

added theorem IsLprojection.mul_compl_self

added structure IsLprojection

added structure IsMprojection