Theorem IsLprojection.coe_inf

Modification history

2023-03-23 16:06

Mathlib/Analysis/NormedSpace/MStructure.lean

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

Added IsLprojection.coe_inf View on Github →