Structures · Analysis
Submodule.HasOrthogonalProjection
A subspace K : Submodule 𝕜 E has an orthogonal projection if every vector v : E admits an
orthogonal projection to K.
- Shape
- One type argument · adds exists_orthogonal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Real
How is a type an instance?
Loading the hierarchy index…
Assumed by252
- Submodule.orthogonalProjectionOnto
- Submodule.starProjection
- EuclideanGeometry.orthogonalProjection
- Submodule.reflection
- EuclideanGeometry.reflection
- Submodule.isCompl_orthogonal
- EuclideanGeometry.orthogonalProjection_mem
- Submodule.orthogonalDecomposition
- EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal
- Submodule.orthogonal_orthogonal
- EuclideanGeometry.orthogonalProjection_eq_self_iff
- AffineSubspace.signedInfDist
- Submodule.starProjection_eq_self_iff
- Submodule.orthogonalProjectionOnto_apply_of_mem_orthogonal
- Submodule.orthogonalProjectionOnto_mem_subspace_eq_self
- EuclideanGeometry.orthogonalProjection_congr
- Submodule.sub_starProjection_mem_orthogonal
- Submodule.starProjection_inner_eq_zero
- Submodule.quotientEquivOrthogonal
- Submodule.orthogonal_eq_bot_iff
- Submodule.starProjection_apply
- Submodule.starProjection_orthogonal_val
- EuclideanGeometry.reflection_apply'
- Submodule.orthogonalProjectionOnto_norm_le
- Submodule.eq_starProjection_of_mem_of_inner_eq_zero
- Submodule.orthogonalDecomposition_apply
- Submodule.inner_orthogonalProjectionOnto_eq_of_mem_right
- EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq
- EuclideanGeometry.dist_orthogonalProjection_eq_infDist
- EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem
- Submodule.inner_orthogonalProjectionOnto_eq_of_mem_left
- EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq
- EuclideanGeometry.angle_self_orthogonalProjection
- EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
- Submodule.reflection_mem_subspace_eq_self
- Submodule.isSymmetricProjection_starProjection
- Submodule.orthogonalProjectionOnto_starProjection_of_le
- Submodule.norm_orthogonalProjectionOnto_apply
- Submodule.norm_sq_eq_add_norm_sq_starProjection
- Submodule.orthogonalProjectionOnto_orthogonal_apply_eq_zero
- Submodule.isIdempotentElem_starProjection
- Submodule.lipschitzWith_orthogonalProjectionOnto
- EuclideanGeometry.orthogonalProjection_mem_orthogonal
- Submodule.orthogonalProjectionFn
- Submodule.inner_starProjection_left_eq_right
- EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt
- EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq
- ClosedSubmodule.orthogonal_orthogonal_eq
- Submodule.starProjection_isSymmetric
- Submodule.reflection_apply
Ancestors0
No ancestors.