Theorems · Theorem · functional analysis
Submodule.isCompl_orthogonal
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(K : Submodule 𝕜 E) [K.HasOrthogonalProjection], IsCompl K KᗮIf K admits an orthogonal projection, K and Kᗮ are complements of each other.
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NormedAddCommGroupstatement and proof · cited by 15,752
- Submodulestatement and proof · cited by 7,192
- InnerProductSpacestatement and proof · cited by 3,523
- RCLikestatement and proof · cited by 2,829
- IsComplstatement · cited by 351
- Submodule.orthogonalstatement and proof · cited by 257
- Submodule.HasOrthogonalProjectionstatement and proof · cited by 245
- add_sub_cancelproof · cited by 195
- Submodule.orthogonal_disjointproof · cited by 6
- Submodule.codisjoint_iff_exists_add_eqproof · cited by 2
- Submodule.HasOrthogonalProjection.exists_orthogonalproof · cited by 1
Cited by26
Results whose statement or proof uses this declaration.
- Submodule.orthogonalDecompositionproof · cited by 14
- Submodule.starProjection_inner_eq_zeroproof · cited by 8
- Submodule.quotientEquivOrthogonalproof · cited by 7
- Submodule.orthogonalDecomposition_applyproof · cited by 6
- EuclideanGeometry.inter_eq_singleton_orthogonalProjectionproof · cited by 2
- Submodule.quotientEquivOrthogonal_mkproof · cited by 1
- Submodule.toLinearMap_orthogonalProjectionOnto_eq_projectionOntostatement · cited by 1
- Submodule.orthogonalProjectionOnto_apply_eq_projectionOntostatement · cited by 1
- Submodule.norm_projection_orthogonal_lestatement and proof · cited by 1
- LinearMap.IsSymmetricProjection.le_iff_range_le_rangeproof · cited by 1
- Submodule.det_reflectionproof · cited by 1
- Submodule.isTopCompl_orthogonalproof · cited by 1