Documentation Verification Report

Bases

📁 Source: Mathlib/Analysis/Normed/Module/Bases.lean

Statistics

Metric	Count
Definitions `GeneralSchauderBasis`, `basis`, `coord`, `proj`, `SchauderBasis`, `RankOneDecomposition`, `P`, `basis`, `basisCoeff`, `e`, `enormProjBound`, `nnnormProjBound`, `proj`, `succSub`, `UnconditionalSchauderBasis`, `enormProjBound`, `nnnormProjBound`, `instCoeFunGeneralSchauderBasisForall`	18
Theorems `expansion`, `ext`, `ext_iff`, `finrank_range_proj`, `linearIndependent`, `ortho`, `proj_apply`, `proj_apply_basis_mem`, `proj_comp`, `proj_empty`, `range_proj_eq_span`, `tendsto_proj`, `basisCoeff_spec`, `basis_coe`, `basis_proj`, `e_mem_range`, `e_ne_zero`, `exists_coeff`, `finrank_range`, `proj_comp`, `proj_tendsto`, `proj_zero`, `bddAbove_range_nnnorm_proj`, `enorm_proj_le_enormProjBound`, `exists_norm_proj_le`, `finrank_range_proj`, `finrank_range_succSub_eq_one`, `nnnorm_proj_le_nnnormProjBound`, `norm_proj_le_nnnormProjBound`, `proj_apply`, `proj_apply_basis_mem`, `proj_comp`, `proj_zero`, `range_proj_eq_span`, `succSub_ortho`, `sum_succSub`, `tendsto_proj`, `bddAbove_range_nnnorm_proj`, `enorm_proj_le_enormProjBound`, `exists_norm_proj_le`, `nnnorm_proj_le_nnnormProjBound`, `norm_proj_le_nnnormProjBound`	42
Total	60

GeneralSchauderBasis

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	11 math math: `proj_apply`, `SchauderBasis.range_proj_eq_span`, `expansion`, `proj_apply_basis_mem`, `SchauderBasis.proj_apply`, `ext_iff`, `SchauderBasis.proj_apply_basis_mem`, `ortho`, `SchauderBasis.RankOneDecomposition.basis_coe`, `range_proj_eq_span`, `linearIndependent`
`coord` 📖	CompOp	5 math math: `proj_apply`, `expansion`, `SchauderBasis.proj_apply`, `ext_iff`, `ortho`
`proj` 📖	CompOp	12 math math: `tendsto_proj`, `proj_apply`, `UnconditionalSchauderBasis.enorm_proj_le_enormProjBound`, `proj_apply_basis_mem`, `UnconditionalSchauderBasis.norm_proj_le_nnnormProjBound`, `proj_empty`, `UnconditionalSchauderBasis.bddAbove_range_nnnorm_proj`, `UnconditionalSchauderBasis.nnnorm_proj_le_nnnormProjBound`, `range_proj_eq_span`, `proj_comp`, `UnconditionalSchauderBasis.exists_norm_proj_le`, `finrank_range_proj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`expansion` 📖	mathematical	—	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `NormedSpace.toModule` `DFunLike.coe` `StrongDual` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `coord` `basis`	—	—
`ext` 📖	—	`basis` `coord`	—	—	—
`ext_iff` 📖	mathematical	—	`basis` `coord`	—	`ext`
`finrank_range_proj` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `proj` `Submodule.addCommMonoid` `Submodule.module` `Finset.card`	—	`RingHomSurjective.ids` `range_proj_eq_span` `Set.image_eq_range` `finrank_span_eq_card` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LinearIndependent.comp` `linearIndependent` `Subtype.val_injective` `Fintype.card_coe`
`linearIndependent` 📖	mathematical	—	`LinearIndependent` `basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule`	—	`linearIndependent_iff` `Finsupp.ext` `Finsupp.linearCombination_apply` `Finset.sum_congr` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ortho` `Pi.single_apply` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq` `map_zero` `AddMonoidHomClass.toZeroHomClass`
`ortho` 📖	mathematical	—	`DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `coord` `basis` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	—
`proj_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `proj` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `StrongDual` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `coord` `basis`	—	`ContinuousLinearMap.sum_apply` `Finset.sum_congr`
`proj_apply_basis_mem` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `proj` `basis` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.decidableMem` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`proj_apply` `Finset.sum_congr` `ortho` `Pi.single_apply` `ite_smul` `one_smul` `zero_smul` `Finset.sum_ite_eq'`
`proj_comp` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `proj` `Finset` `Finset.instInter`	—	`proj_apply` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ortho` `Pi.single_apply` `ite_smul` `one_smul` `zero_smul` `Finset.sum_ite_eq'` `smul_ite` `smul_zero` `Finset.sum_ite_mem` `Finset.ext`
`proj_empty` 📖	mathematical	—	`proj` `Finset` `Finset.instEmptyCollection` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.zero`	—	—
`range_proj_eq_span` 📖	mathematical	—	`LinearMap.range` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `proj` `Submodule.span` `Set.image` `basis` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`le_antisymm` `RingHomSurjective.ids` `ContinuousLinearMap.coe_coe` `proj_apply` `Submodule.sum_mem` `Submodule.smul_mem` `Submodule.subset_span` `Submodule.span_le` `proj_apply_basis_mem` `Finset.mem_coe`
`tendsto_proj` 📖	mathematical	—	`Filter.Tendsto` `Finset` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `proj` `SummationFilter.filter` `nhds`	—	`proj_apply` `expansion`

SchauderBasis

Definitions

Name	Category	Theorems
`RankOneDecomposition` 📖	CompData	—
`enormProjBound` 📖	CompOp	1 math math: `enorm_proj_le_enormProjBound`
`nnnormProjBound` 📖	CompOp	2 math math: `norm_proj_le_nnnormProjBound`, `nnnorm_proj_le_nnnormProjBound`
`proj` 📖	CompOp	13 math math: `norm_proj_le_nnnormProjBound`, `tendsto_proj`, `proj_zero`, `RankOneDecomposition.basis_proj`, `range_proj_eq_span`, `finrank_range_proj`, `proj_apply`, `bddAbove_range_nnnorm_proj`, `exists_norm_proj_le`, `proj_comp`, `proj_apply_basis_mem`, `nnnorm_proj_le_nnnormProjBound`, `enorm_proj_le_enormProjBound`
`succSub` 📖	CompOp	6 math math: `RankOneDecomposition.basisCoeff_spec`, `finrank_range_succSub_eq_one`, `RankOneDecomposition.exists_coeff`, `succSub_ortho`, `RankOneDecomposition.e_mem_range`, `sum_succSub`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_range_nnnorm_proj` 📖	mathematical	—	`BddAbove` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `Set.range` `NNNorm.nnnorm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `proj`	—	`RingHomIsometric.ids` `exists_norm_proj_le` `proj_zero` `norm_zero` `NNReal.coe_le_coe` `Real.coe_toNNReal` `coe_nnnorm`
`enorm_proj_le_enormProjBound` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENorm.enorm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddGroup.toContinuousENorm` `proj` `enormProjBound`	—	`le_iSup` `RingHomIsometric.ids`
`exists_norm_proj_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.hasOpNorm` `proj`	—	`banach_steinhaus` `RingHomIsometric.ids` `isBounded_iff_forall_norm_le` `Metric.isBounded_range_of_tendsto` `tendsto_proj` `Set.forall_mem_range`
`finrank_range_proj` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `proj` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `proj.eq_1` `GeneralSchauderBasis.finrank_range_proj` `Finset.card_range`
`finrank_range_succSub_eq_one` 📖	mathematical	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.funLike`	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `succSub` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `inf_of_le_right` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Submodule.sub_mem` `le_antisymm` `ContinuousLinearMap.coe_coe` `sub_add_cancel` `Submodule.add_mem_sup` `sup_le` `eq_bot_iff` `min_self` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `inf_of_le_left` `sub_self` `FiniteDimensional.of_finrank_pos` `Submodule.finiteDimensional_of_le` `Submodule.finrank_sup_add_finrank_inf_eq` `add_zero` `finrank_bot` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`nnnorm_proj_le_nnnormProjBound` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `NNNorm.nnnorm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `proj` `nnnormProjBound`	—	`le_ciSup` `RingHomIsometric.ids` `bddAbove_range_nnnorm_proj`
`norm_proj_le_nnnormProjBound` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.hasOpNorm` `proj` `NNReal.toReal` `nnnormProjBound`	—	`nnnorm_proj_le_nnnormProjBound`
`proj_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `proj` `Finset.sum` `Finset.range` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `StrongDual` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `GeneralSchauderBasis.coord` `SummationFilter.conditional` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `GeneralSchauderBasis.basis`	—	`proj.eq_1` `GeneralSchauderBasis.proj_apply`
`proj_apply_basis_mem` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `proj` `GeneralSchauderBasis.basis` `SummationFilter.conditional` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`proj.eq_1` `GeneralSchauderBasis.proj_apply_basis_mem`
`proj_comp` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `proj`	—	`GeneralSchauderBasis.proj_comp` `Finset.ext`
`proj_zero` 📖	mathematical	—	`proj` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.zero`	—	`proj.eq_1` `Finset.range_zero` `GeneralSchauderBasis.proj_empty`
`range_proj_eq_span` 📖	mathematical	—	`LinearMap.range` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `proj` `Submodule.span` `Set.image` `GeneralSchauderBasis.basis` `SummationFilter.conditional` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.range`	—	`RingHomSurjective.ids` `proj.eq_1` `GeneralSchauderBasis.range_proj_eq_span`
`succSub_ortho` 📖	mathematical	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `succSub` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `min_self` `min_eq_right` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg` `add_zero` `min_eq_left_of_lt` `min_eq_left` `min_eq_right_of_lt`
`sum_succSub` 📖	mathematical	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.zero`	`Finset.sum` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.range` `succSub`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.sum_range_succ` `succSub.eq_1` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `RingHomIsometric.ids` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `zero_add` `Mathlib.Tactic.Abel.zero_termg`
`tendsto_proj` 📖	mathematical	—	`Filter.Tendsto` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `proj` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`GeneralSchauderBasis.tendsto_proj` `SummationFilter.conditional_filter_eq_map_range`

SchauderBasis.RankOneDecomposition

Definitions

Name	Category	Theorems
`P` 📖	CompOp	8 math math: `proj_tendsto`, `basis_proj`, `basisCoeff_spec`, `finrank_range`, `proj_zero`, `exists_coeff`, `proj_comp`, `e_mem_range`
`basis` 📖	CompOp	2 math math: `basis_proj`, `basis_coe`
`basisCoeff` 📖	CompOp	1 math math: `basisCoeff_spec`
`e` 📖	CompOp	4 math math: `basisCoeff_spec`, `exists_coeff`, `basis_coe`, `e_mem_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basisCoeff_spec` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `basisCoeff` `e` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `SchauderBasis.succSub` `P`	—	`exists_coeff`
`basis_coe` 📖	mathematical	—	`GeneralSchauderBasis.basis` `SummationFilter.conditional` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `basis` `e`	—	—
`basis_proj` 📖	mathematical	—	`SchauderBasis.proj` `basis` `P`	—	`ContinuousLinearMap.ext` `SchauderBasis.proj_apply` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SchauderBasis.sum_succSub` `proj_zero` `ContinuousLinearMap.coe_sum'` `Finset.sum_apply` `Finset.sum_congr` `basisCoeff_spec`
`e_mem_range` 📖	mathematical	—	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `SchauderBasis.succSub` `P` `e`	—	—
`e_ne_zero` 📖	—	—	—	—	—
`exists_coeff` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `e` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `SchauderBasis.succSub` `P`	—	`RingHomSurjective.ids` `SchauderBasis.finrank_range_succSub_eq_one` `finrank_range` `proj_comp` `FiniteDimensional.of_finrank_pos` `zero_lt_one` `Nat.instZeroLEOneClass` `Submodule.eq_of_le_of_finrank_eq` `Submodule.span_singleton_le_iff_mem` `e_mem_range` `finrank_span_singleton` `e_ne_zero` `Submodule.mem_span_singleton` `LinearMap.mem_range_self`
`finrank_range` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `P` `Submodule.addCommMonoid` `Submodule.module`	—	—
`proj_comp` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `P`	—	—
`proj_tendsto` 📖	mathematical	—	`Filter.Tendsto` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `P` `Filter.atTop` `Nat.instPreorder` `nhds`	—	—
`proj_zero` 📖	mathematical	—	`P` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.zero`	—	—

UnconditionalSchauderBasis

Definitions

Name	Category	Theorems
`enormProjBound` 📖	CompOp	1 math math: `enorm_proj_le_enormProjBound`
`nnnormProjBound` 📖	CompOp	2 math math: `norm_proj_le_nnnormProjBound`, `nnnorm_proj_le_nnnormProjBound`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_range_nnnorm_proj` 📖	mathematical	—	`BddAbove` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `Set.range` `Finset` `NNNorm.nnnorm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `GeneralSchauderBasis.proj` `SummationFilter.unconditional`	—	`RingHomIsometric.ids` `exists_norm_proj_le` `GeneralSchauderBasis.proj_empty` `norm_zero` `NNReal.coe_le_coe` `Real.coe_toNNReal` `coe_nnnorm`
`enorm_proj_le_enormProjBound` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENorm.enorm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddGroup.toContinuousENorm` `GeneralSchauderBasis.proj` `SummationFilter.unconditional` `enormProjBound`	—	`le_iSup` `RingHomIsometric.ids`
`exists_norm_proj_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.hasOpNorm` `GeneralSchauderBasis.proj` `SummationFilter.unconditional`	—	`banach_steinhaus` `RingHomIsometric.ids` `summable_iff_vanishing_norm` `HasSum.summable` `GeneralSchauderBasis.expansion` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.one` `Real.instNontrivial` `Finset.Nonempty.image` `Finset.powerset_nonempty` `GeneralSchauderBasis.proj_apply` `Finset.sum_union` `Disjoint.symm` `Finset.disjoint_sdiff_inter` `Finset.union_comm` `Finset.sdiff_union_inter` `Finset.sdiff_disjoint` `LE.le.trans` `norm_add_le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Finset.le_sup'` `Finset.mem_image_of_mem` `Finset.mem_powerset` `Finset.inter_subset_right` `LT.lt.le`
`nnnorm_proj_le_nnnormProjBound` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `NNNorm.nnnorm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `GeneralSchauderBasis.proj` `SummationFilter.unconditional` `nnnormProjBound`	—	`le_ciSup` `RingHomIsometric.ids` `bddAbove_range_nnnorm_proj`
`norm_proj_le_nnnormProjBound` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.hasOpNorm` `GeneralSchauderBasis.proj` `SummationFilter.unconditional` `NNReal.toReal` `nnnormProjBound`	—	`nnnorm_proj_le_nnnormProjBound`

(root)

Definitions

Name	Category	Theorems
`GeneralSchauderBasis` 📖	CompData	—
`SchauderBasis` 📖	CompOp	—
`UnconditionalSchauderBasis` 📖	CompOp	—
`instCoeFunGeneralSchauderBasisForall` 📖	CompOp	—

---

← Back to Index