Subspace

📁 Source: Mathlib/Analysis/InnerProductSpace/Subspace.lean

Statistics

Metric	Count
Definitions OrthogonalFamily, innerProductSpace	2
Theorems collectedBasis_orthonormal, comp, eq_ite, independent, inner_right_dfinsupp, inner_right_fintype, inner_sum, norm_sq_diff_sum, norm_sum, orthonormal_sigma_orthonormal, summable_iff_norm_sq_summable, codRestrict, orthogonalFamily, coe_inner, orthonormal_span	15
Total	17

DirectSum.IsInternal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
collectedBasis_orthonormal 📖	mathematical	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace Submodule.subtypeₗᵢ DirectSum.IsInternal Submodule.addSubmonoidClass Orthonormal DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.module Module.Basis.instFunLike	collectedBasis	—	Submodule.addSubmonoidClass collectedBasis_coe OrthogonalFamily.orthonormal_sigma_orthonormal

OrthogonalFamily

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup	—	—	—
eq_ite 📖	mathematical	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup	Inner.inner InnerProductSpace.toInner DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule InnerProductSpace.toNormedSpace LinearIsometry.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	—
independent 📖	mathematical	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace Submodule.subtypeₗᵢ	iSupIndep Submodule.completeLattice	—	iSupIndep_of_dfinsupp_lsum_injective RingHomInvPair.ids AddMonoid.nat_smulCommClass' LinearMap.ker_eq_bot Submodule.eq_bot_iff DFinsupp.ext DFinsupp.sumAddHom_apply inner_right_dfinsupp LinearMap.mem_ker inner_zero_right
inner_right_dfinsupp 📖	mathematical	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup	Inner.inner InnerProductSpace.toInner DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule InnerProductSpace.toNormedSpace LinearIsometry.instFunLike DFinsupp.sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup DFinsupp DFinsupp.instDFunLike	—	DFinsupp.inner_sum eq_ite Finset.sum_congr Finset.sum_ite_eq LinearIsometry.inner_map_map of_not_not inner_zero_right
inner_right_fintype 📖	mathematical	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup	Inner.inner InnerProductSpace.toInner DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule InnerProductSpace.toNormedSpace LinearIsometry.instFunLike Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Finset.univ	—	inner_sum eq_ite Finset.sum_ite_eq LinearIsometry.inner_map_map
inner_sum 📖	mathematical	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup	Inner.inner InnerProductSpace.toInner Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule InnerProductSpace.toNormedSpace LinearIsometry.instFunLike ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	inner_sum Finset.sum_congr sum_inner eq_ite Finset.sum_ite_eq' LinearIsometry.inner_map_map Finset.sum_ite_of_true
norm_sq_diff_sum 📖	mathematical	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup	Real Monoid.toNatPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule InnerProductSpace.toNormedSpace LinearIsometry.instFunLike Real.instAdd Real.instAddCommMonoid Finset Finset.instSDiff NormedAddCommGroup.toNorm	—	Finset.sum_sdiff_sub_sum_sdiff sub_eq_add_neg Finset.sum_neg_distrib Finset.sdiff_subset Finset.mem_sdiff norm_neg disjoint_sdiff_sdiff Finset.sum_union norm_sum Finset.sum_congr LinearIsometry.map_neg
norm_sum 📖	mathematical	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup	Real Monoid.toNatPow Real.instMonoid Norm.norm SeminormedAddCommGroup.toNorm Finset.sum AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule InnerProductSpace.toNormedSpace LinearIsometry.instFunLike Real.instAddCommMonoid NormedAddCommGroup.toNorm	—	inner_sum Finset.sum_congr Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing
orthonormal_sigma_orthonormal 📖	mathematical	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup Orthonormal	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule InnerProductSpace.toNormedSpace LinearIsometry.instFunLike	—	LinearIsometry.norm_map LinearIsometry.inner_map_map
summable_iff_norm_sq_summable 📖	mathematical	OrthogonalFamily NormedAddCommGroup.toSeminormedAddCommGroup	Summable AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule InnerProductSpace.toNormedSpace LinearIsometry.instFunLike SummationFilter.unconditional Real Real.instAddCommMonoid Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	Real.instCompleteSpace Real.sqrt_pos Finset.sum_sdiff_sub_sum_sdiff LE.le.trans_lt abs_sub Real.instIsOrderedAddMonoid sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Finset.abs_sum_of_nonneg' norm_sq_diff_sum sq_lt_sq Real.instIsStrictOrderedRing abs_of_nonneg Real.sqrt_nonneg norm_nonneg Real.sq_sqrt le_of_lt lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le Nat.instAtLeastTwoHAddOfNat half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono sq_pos_of_pos abs_lt_of_sq_lt_sq' le_inf Finset.inter_subset_left Finset.sum_sdiff add_tsub_cancel_right AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Finset.sum_congr Finset.sdiff_inter_self_left Finset.inter_subset_right Finset.sdiff_inter_self_right Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Linarith.add_neg CancelDenoms.sub_subst CancelDenoms.div_subst CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_nonpos

Orthonormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict 📖	mathematical	Orthonormal Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike	Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace Set.codRestrict SetLike.coe	—	LinearIsometry.orthonormal_comp_iff
orthogonalFamily 📖	mathematical	Orthonormal	OrthogonalFamily NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.innerProductSpace LinearIsometry.toSpanSingleton DenselyNormedField.toNontriviallyNormedField InnerProductSpace.toNormedSpace Pairwise Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	—	inner_smul_right inner_smul_left MulZeroClass.mul_zero

Submodule

Definitions

Name	Category	Theorems
innerProductSpace 📖	CompOp	50 math math: TensorProduct.mapInclIsometry_apply, Affine.Simplex.altitudeFoot_restrict, OrthonormalBasis.orthogonalProjection_eq_sum, Orthonormal.codRestrict, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, OrthogonalFamily.of_pairwise, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, Affine.Simplex.circumradius_restrict, Affine.Simplex.ninePointCircle_restrict, OrthonormalBasis.orthogonalProjection_apply_eq_sum, EuclideanGeometry.Sphere.coe_secondInter, adjoint_subtypeL, HilbertBasis.hasSum_orthogonalProjection, Affine.Simplex.altitude_restrict_eq_comap_subtype, OrthonormalBasis.starProjection_eq_sum_rankOne, TensorProduct.inner_mapIncl_mapIncl, LinearMap.IsSymmetric.restrict_invariant, Affine.Simplex.ExcenterExists.touchpointWeights_restrict, EuclideanGeometry.orthogonalProjection_subtype, Affine.Simplex.ExcenterExists.excenter_restrict, Affine.Simplex.map_altitude_restrict, orthogonalFamily_self, Affine.Simplex.exradius_restrict, inner_orthogonalProjection_eq_of_mem_right, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace, Affine.Simplex.circumcenter_restrict, Affine.Simplex.height_restrict, coe_inner, Affine.Simplex.incenter_restrict, inner_orthogonalProjection_eq_of_mem_left, Affine.Simplex.inradius_restrict, Affine.Simplex.orthogonalProjectionSpan_restrict, Affine.Simplex.excenterWeights_restrict, Affine.Simplex.mongePoint_restrict, Affine.Simplex.eulerPoint_restrict, OrthonormalBasis.span_apply, Affine.Simplex.ExcenterExists.touchpoint_restrict, Affine.Simplex.excenterWeightsUnnorm_restrict, ContinuousLinearMap.IsPositive.orthogonalProjection_comp, adjoint_orthogonalProjection, orthogonalFamily_iff_pairwise, angle_coe, AffineSubspace.angle_coe, EuclideanGeometry.reflection_subtype, LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces, TensorProduct.toLinearMap_mapInclIsometry, orthonormal_span, isHilbertSumOrthogonal, Affine.Simplex.excenterExists_restrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_inner 📖	mathematical	—	Inner.inner Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike InnerProductSpace.toInner seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing innerProductSpace	—	—

(root)

Definitions

Name	Category	Theorems
OrthogonalFamily 📖	MathDef	9 math math: OrthogonalFamily.of_pairwise, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, IsHilbertSum.OrthogonalFamily, Submodule.orthogonalFamily_self, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace, Orthonormal.orthogonalFamily, orthogonalFamily_iff_pairwise, LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orthonormal_span 📖	mathematical	Orthonormal	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.span Set.range Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace Submodule.subset_span Set.mem_range_self	—	Orthonormal.codRestrict Submodule.subset_span Set.mem_range_self

---

← Back to Index