Theorem UnconditionalSchauderBasis.norm_proj_le_nnnormProjBound

Modification history

2026-03-17 20:24
Mathlib/Analysis/Normed/Module/Bases.lean
feat(Analysis/Normed): Schauder basis definition and characterization via projections (#34209) …
Added UnconditionalSchauderBasis.norm_proj_le_nnnormProjBoundView on Github →