Theorems · Definition · functional analysis
SchauderBasis
(𝕜 : Type u_4) →
(X : Type u_5) →
[inst : NontriviallyNormedField 𝕜] →
[inst_1 : NormedAddCommGroup X] → [NormedSpace 𝕜 X] → Type (max (max 0 u_4) u_5)A classical Schauder basis indexed by ℕ with conditional convergence.
- Defined in
- Mathlib.Analysis.Normed.Module.Bases
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- GeneralSchauderBasisproof · cited by 16
- SummationFilter.conditionalproof · cited by 13
Cited by17
Results whose statement or proof uses this declaration.
- SchauderBasis.projstatement and proof · cited by 13
- SchauderBasis.nnnormProjBoundstatement and proof · cited by 2
- SchauderBasis.RankOneDecomposition.basisstatement · cited by 2
- HilbertBasis.toSchauderBasisstatement · cited by 2
- SchauderBasis.bddAbove_range_nnnorm_projstatement and proof · cited by 1
- SchauderBasis.enormProjBoundstatement and proof · cited by 1
- SchauderBasis.exists_norm_proj_lestatement and proof · cited by 1
- SchauderBasis.nnnorm_proj_le_nnnormProjBoundstatement and proof · cited by 1
- SchauderBasis.proj_applystatement and proof · cited by 1
- SchauderBasis.proj_zerostatement and proof · cited by 1
- SchauderBasis.tendsto_projstatement and proof · cited by 1
- SchauderBasis.enorm_proj_le_enormProjBoundstatement and proof · cited by 0