Submodule

📁 Source: Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean

Statistics

Metric	Count
Definitions	0
Theorems orthogonal_eq_orthogonal_iff, orthogonal_injective, orthogonal_orthogonal_eq, sup_orthogonal, eq_of_inner_left, eq_of_inner_right, eq_of_sub_mem_orthogonal, eq_zero_of_inner_left, eq_zero_of_inner_right, eq_zero_of_mem_orthogonal, isCompl_orthogonal_of_hasOrthogonalProjection, le_orthogonal_iff_le_orthogonal, orthogonalComplement_eq_orthogonalComplement, orthogonalProjection_apply_eq_linearProjOfIsCompl, orthogonalProjection_coe_eq_linearProjOfIsCompl, orthogonalProjection_eq_linearProjOfIsCompl, orthogonal_eq_bot_iff, orthogonal_le_iff_orthogonal_le, orthogonal_le_orthogonal_iff, orthogonal_orthogonal, orthogonal_orthogonal_eq_closure, starProjection_apply_eq_isComplProjection, starProjection_coe_eq_isCompl_projection, starProjection_tendsto_closure_iSup, starProjection_tendsto_self, sup_orthogonal_inf_of_hasOrthogonalProjection, sup_orthogonal_of_hasOrthogonalProjection, toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl, toLinearMap_starProjection_eq_isComplProjection, topologicalClosure_eq_top_iff, triorthogonal_eq_orthogonal	31
Total	31

ClosedSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orthogonal_eq_orthogonal_iff 📖	mathematical	—	orthogonal	—	orthogonal_orthogonal_eq
orthogonal_injective 📖	mathematical	—	ClosedSubmodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace orthogonal	—	orthogonal_eq_orthogonal_iff Submodule.instHasOrthogonalProjectionOfCompleteSpace
orthogonal_orthogonal_eq 📖	mathematical	—	orthogonal	—	ext Set.ext Submodule.orthogonal_orthogonal
sup_orthogonal 📖	mathematical	—	ClosedSubmodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace instMax IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul orthogonal instInf	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul orthogonal_orthogonal_eq Submodule.instHasOrthogonalProjectionOfCompleteSpace inf_orthogonal

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_inner_left 📖	—	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike Inner.inner InnerProductSpace.toInner SetLike.instMembership	—	—	eq_of_sub_mem_orthogonal Submodule.sub_mem_orthogonal_of_inner_left
eq_of_inner_right 📖	—	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike Inner.inner InnerProductSpace.toInner SetLike.instMembership	—	—	eq_of_sub_mem_orthogonal Submodule.sub_mem_orthogonal_of_inner_right
eq_of_sub_mem_orthogonal 📖	—	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike SetLike.instMembership Submodule.orthogonal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	—	sub_eq_zero eq_zero_of_mem_orthogonal
eq_zero_of_inner_left 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike Inner.inner InnerProductSpace.toInner SetLike.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Continuous.ext_on TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.inner continuous_const continuous_id inner_self_eq_norm_sq_to_K isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat IsLocalRing.toNontrivial Field.instIsLocalRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
eq_zero_of_inner_right 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike Inner.inner InnerProductSpace.toInner SetLike.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	eq_of_inner_right inner_zero_right
eq_zero_of_mem_orthogonal 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike SetLike.instMembership Submodule.orthogonal	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	eq_zero_of_inner_left Submodule.mem_orthogonal'

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompl_orthogonal_of_hasOrthogonalProjection 📖	mathematical	—	IsCompl Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace instPartialOrder CompleteLattice.toBoundedOrder completeLattice orthogonal	—	orthogonal_disjoint codisjoint_iff sup_orthogonal_of_hasOrthogonalProjection
le_orthogonal_iff_le_orthogonal 📖	mathematical	—	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder orthogonal	—	orthogonal_le_orthogonal_iff instHasOrthogonalProjectionOrthogonal orthogonal_orthogonal
orthogonalComplement_eq_orthogonalComplement 📖	mathematical	—	orthogonal	—	orthogonal_orthogonal
orthogonalProjection_apply_eq_linearProjOfIsCompl 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection LinearMap Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup LinearMap.instFunLike linearProjOfIsCompl orthogonal isCompl_orthogonal_of_hasOrthogonalProjection	—	isCompl_orthogonal_of_hasOrthogonalProjection IsCompl.symm IsCompl.projection_add_projection_eq_self map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass orthogonalProjection_mem_subspace_eq_self orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero coe_mem add_zero
orthogonalProjection_coe_eq_linearProjOfIsCompl 📖	mathematical	—	ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module orthogonalProjection linearProjOfIsCompl NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup orthogonal isCompl_orthogonal_of_hasOrthogonalProjection	—	toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl
orthogonalProjection_eq_linearProjOfIsCompl 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection LinearMap Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup LinearMap.instFunLike linearProjOfIsCompl orthogonal isCompl_orthogonal_of_hasOrthogonalProjection	—	orthogonalProjection_apply_eq_linearProjOfIsCompl
orthogonal_eq_bot_iff 📖	mathematical	—	orthogonal Bot.bot Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace instBot Top.top instTop	—	sup_orthogonal_of_hasOrthogonalProjection bot_sup_eq sup_comm top_orthogonal_eq_bot
orthogonal_le_iff_orthogonal_le 📖	mathematical	—	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder orthogonal	—	orthogonal_le_orthogonal_iff instHasOrthogonalProjectionOrthogonal orthogonal_orthogonal
orthogonal_le_orthogonal_iff 📖	mathematical	—	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder orthogonal	—	orthogonal_orthogonal orthogonal_le
orthogonal_orthogonal 📖	mathematical	—	orthogonal	—	ext exists_add_mem_mem_orthogonal inner_add_right inner_self_eq_norm_sq_to_K zero_add isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat IsLocalRing.toNontrivial Field.instIsLocalRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass add_zero inner_eq_zero_symm
orthogonal_orthogonal_eq_closure 📖	mathematical	—	orthogonal topologicalClosure DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	le_antisymm UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup orthogonal_orthogonal HasOrthogonalProjection.ofCompleteSpace topologicalClosure.completeSpace orthogonal_orthogonal_monotone le_topologicalClosure topologicalClosure_minimal le_orthogonal_orthogonal isClosed_orthogonal
starProjection_apply_eq_isComplProjection 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace ContinuousLinearMap.funLike starProjection LinearMap Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup LinearMap.instFunLike IsCompl.projection orthogonal isCompl_orthogonal_of_hasOrthogonalProjection	—	isCompl_orthogonal_of_hasOrthogonalProjection toLinearMap_starProjection_eq_isComplProjection
starProjection_coe_eq_isCompl_projection 📖	mathematical	—	ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace starProjection IsCompl.projection NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup orthogonal isCompl_orthogonal_of_hasOrthogonalProjection	—	toLinearMap_starProjection_eq_isComplProjection
starProjection_tendsto_closure_iSup 📖	mathematical	HasOrthogonalProjection Monotone Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace PartialOrder.toPreorder instPartialOrder	Filter.Tendsto DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection Filter.atTop nhds topologicalClosure UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Tendsto.of_neBot_imp Filter.atTop_neBot_iff orthogonalProjection_starProjection_of_le LE.le.trans le_iSup le_topologicalClosure coe_mem Metric.mem_closure_iff topologicalClosure_coe SetLike.mem_coe mem_iSup_of_directed Monotone.directed_le norm_sub_rev starProjection_minimal lt_of_le_of_lt ciInf_le Set.forall_mem_range norm_nonneg dist_eq_norm
starProjection_tendsto_self 📖	mathematical	HasOrthogonalProjection Monotone Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace PartialOrder.toPreorder instPartialOrder Preorder.toLE Top.top instTop topologicalClosure UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	Filter.Tendsto DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection Filter.atTop nhds	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup top_unique instHasOrthogonalProjectionTop starProjection_eq_self_iff starProjection_tendsto_closure_iSup
sup_orthogonal_inf_of_hasOrthogonalProjection 📖	mathematical	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instMin orthogonal	—	ext mem_sup sub_starProjection_mem_orthogonal add_mem Subtype.prop sub_mem add_sub_cancel
sup_orthogonal_of_hasOrthogonalProjection 📖	mathematical	—	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice orthogonal Top.top instTop	—	inf_of_le_left sup_orthogonal_inf_of_hasOrthogonalProjection le_top
toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl 📖	mathematical	—	ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module orthogonalProjection linearProjOfIsCompl NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup orthogonal isCompl_orthogonal_of_hasOrthogonalProjection	—	LinearMap.ext isCompl_orthogonal_of_hasOrthogonalProjection orthogonalProjection_apply_eq_linearProjOfIsCompl
toLinearMap_starProjection_eq_isComplProjection 📖	mathematical	—	ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace starProjection IsCompl.projection NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup orthogonal isCompl_orthogonal_of_hasOrthogonalProjection	—	isCompl_orthogonal_of_hasOrthogonalProjection LinearMap.comp.congr_simp toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl
topologicalClosure_eq_top_iff 📖	mathematical	—	topologicalClosure DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup Top.top Submodule instTop orthogonal Bot.bot instBot	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup orthogonal_orthogonal_eq_closure triorthogonal_eq_orthogonal top_orthogonal_eq_bot bot_orthogonal_eq_top
triorthogonal_eq_orthogonal 📖	mathematical	—	orthogonal	—	GaloisConnection.u_l_u_eq_u orthogonal_gc

---

← Back to Index